Determinant Bound application

lemma DeterminantBound.application (hd : 4 ≤ d) (M : ℝ)    (hM : M = sSup {max (b i) (c i) | i ∈ Set.Icc 4 d}) :    ν < 1 + δ - a 3 - M + min (a 3 / 4) (M / 3) := by  have hM' : M ∈ {max (b i) (c i) | i ∈ Set.Icc 4 d} := by    rw [hM]    exact ((Set.nonempty_Icc.2 hd).image _).csSup_mem ((Set.finite_Icc 4 d).image _)  obtain ⟨i, ⟨hi₁, hi₂⟩, hM'⟩ := hM'  wlog hbc : c i ≤ b i generalizing b c  · exact this hdac hdab (by simp [hM, max_comm]) (by simp [hM', max_comm]) (le_of_not_le hbc)  replace hM' : M = b i := by simp [← hM', hbc]  refine hdab.trans_le ?_  refine csInf_le_of_le determinantBound_set_finite.bddBelow    ⟨3, i, by simp; omega, by simp; omega, rfl⟩ ?_  simp only [hM']  gcongr _ + min (_ / ?_) _  · exact ha.nonneg 3  · simpa