Johnson worst case bound

lemma johnson_worst_case_bound {n : ℕ} {F : Type*} [DecidableEq F]    {B : Finset (Fin n → F)} {v : Fin n → F} {d e : ℕ} {frac : ℚ}    (hn_pos : (0 : ℚ) < n) (hd_pos : 0 < d) (d_le_n : d ≤ n)    (h : (e : ℝ) ≤ n - ((n * (n - d)) : ℝ).sqrt)    (h_d_close_n : frac * (d / n : ℚ) ≤ 1)    (hfrac_gt1 : (1 : ℚ) < frac)    (e_ineq : JohnsonBound.e B v ≤ e)    (d_ineq : (d : ℚ) ≤ JohnsonBound.d B)    (quad_nonneg : (0 : ℚ) ≤ (d / n : ℚ) - 2 * (e / n : ℚ) + (e / n : ℚ) ^ 2)    (hden1_pos :      (0 : ℚ) < JohnsonBound.d B / n - 2 * JohnsonBound.e B v / n +        frac * (JohnsonBound.e B v / n) ^ 2) :    (JohnsonBound.d B / n) /      (JohnsonBound.d B / n - 2 * JohnsonBound.e B v / n +      frac * (JohnsonBound.e B v / n) ^ 2) ≤    (d / n) / (d / n - 2 * e / n + frac * (e / n) ^ 2) := by  have h_frac_ineq : (JohnsonBound.d B / n : ℚ) * (d / n - 2 * (e / n) +      frac * (e / n) ^ 2) ≤ (d / n) * (JohnsonBound.d B / n - 2 *        (JohnsonBound.e B v / n) + frac * (JohnsonBound.e B v / n) ^ 2) := by    have h_frac_ineq :        (JohnsonBound.d B / n - d / n) * (2 * (e / n) - frac * (e / n) ^ 2) ≥ 0 ∧        (e / n - JohnsonBound.e B v / n) *          (2 - frac * (e / n + JohnsonBound.e B v / n)) ≥ 0 := by      refine ⟨mul_nonneg ?_ ?_, mul_nonneg ?_ ?_⟩      · exact sub_nonneg_of_le (by gcongr)      · have h_frac_le_one : frac * (e / n : ℚ) ≤ 1 := by          have h_e_le_d : (e / n : ℚ) ≤ (d / n : ℚ) := by            have h_e_le_d : (e : ℝ) ≤ n - √(n * (n - d)) := by grind            have h_e_le_d : (e : ℚ) ≤ d := by              exact_mod_cast (by nlinarith [                show (d : ℝ) ≤ n by norm_cast, sqrt_nonneg (n * (n - d)), mul_self_sqrt (                  show 0 ≤ (n : ℝ) * (n - d) by                  nlinarith [show (d : ℝ) ≤ n by norm_cast])] : (e : ℝ) ≤ d)            gcongr          exact le_trans (mul_le_mul_of_nonneg_left h_e_le_d (by positivity)) h_d_close_n        nlinarith [show 0 ≤ (e : ℚ) / n by positivity]      · exact sub_nonneg_of_le (by gcongr)      · have h_frac_e_n_le_1 : frac * (e / n : ℚ) ≤ 1 := by          refine le_trans (mul_le_mul_of_nonneg_left (show (e : ℚ) / n ≤ d / n from ?_)            (by positivity)) h_d_close_n          have h_e_le_d : (e : ℚ) ≤ d := by            exact_mod_cast (by nlinarith [              show (d : ℝ) ≤ n by norm_cast, sqrt_nonneg (n * (n - d)), mul_self_sqrt (                show 0 ≤ (n : ℝ) * (n - d) by                nlinarith [show (d : ℝ) ≤ n by norm_cast])] : (e : ℝ) ≤ d)          gcongr        have h_frac_e_B_v_n_le_1 : frac * (JohnsonBound.e B v / n : ℚ) ≤ 1 :=          le_trans (mul_le_mul_of_nonneg_left            (div_le_div_of_nonneg_right (show (JohnsonBound.e B v : ℚ) ≤ e by              exact_mod_cast e_ineq) (Nat.cast_nonneg _)) (by positivity)) h_frac_e_n_le_1        linarith    nlinarith [show (0 : ℚ) < n from hn_pos,      mul_div_cancel₀ (e : ℚ) (by positivity : (n : ℚ) ≠ 0),      mul_div_cancel₀ (JohnsonBound.e B v : ℚ) (by positivity : (n : ℚ) ≠ 0),      mul_div_cancel₀ (d : ℚ) (by positivity : (n : ℚ) ≠ 0)]  rw [div_le_div_iff₀] <;> ring_nf at * <;> try linarith  by_cases h_e_zero : e = 0  · aesop  · have h_frac_pos : (n : ℚ)⁻¹ ^ 2 * e ^ 2 * frac > (n : ℚ)⁻¹ ^ 2 * e ^ 2 :=      lt_mul_of_one_lt_right (by positivity) hfrac_gt1    nlinarith [show (e : ℚ) ≥ 1 from by exact_mod_cast Nat.one_le_iff_ne_zero.mpr h_e_zero]