Johnson condition weak implies strong

lemma johnson_condition_weak_implies_strong [Field F]    {B : Finset (Fin n → F)} {v : Fin n → F} {e : ℕ}    (h_J_cond_weak : JohnsonConditionWeak B e)    (h_B2_not_one : 1 < (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)).card)    (h_F_nontriv : 2 ≤ card F) :    JohnsonConditionStrong (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)) v := by  have h_n_pos : 0 < n := by    by_contra hn    push Not at hn    have : n = 0 := by omega    subst this    have B_singleton : B.card ≤ 1 :=      card_le_one.2 (fun _ _ _ _ => funext (Fin.elim0 ·))    have : (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)).card ≤ 1 :=      le_trans (card_le_card inter_subset_left) B_singleton    omega  unfold JohnsonConditionStrong  intro e_1 d q frac  by_cases h_dsqrt_pos : (0 : ℝ) ≤ 1 - frac * d / ↑n  · have h_B2_nonempty : (0 : ℚ) < ((B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)).card : ℚ) :=      by norm_cast; omega    have h_frac_pos : frac > 0 := by      unfold frac      have : 1 < card F := by        simpa [Fintype.one_lt_card_iff] using (⟨(0 : F), (1 : F), by simp⟩ : ∃ a b : F, a ≠ b)      field_simp      unfold q      simp only [Nat.cast_pos, Fintype.zero_lt_card, div_pos_iff_of_pos_left, sub_pos,        Nat.one_lt_cast]      exact h_F_nontriv    have j_fun_bound : (↑e / ↑n : ℝ) < (1 / ↑frac * (1 - √(1 - ↑frac * ↑d / ↑n))) := by      unfold JohnsonConditionWeak J at h_J_cond_weak      simp_all only [Rat.cast_natCast, Rat.cast_div, Rat.cast_sub, Rat.cast_one, one_div, inv_div,        ne_eq, sub_nonneg, Nat.cast_pos, Finset.card_pos, gt_iff_lt]      let d_weak := sInf { d | ∃ u ∈ B, ∃ v ∈ B, ¬u = v ∧ Δ₀(u, v) = d }      have d_subset : ↑d_weak ≤ (d : ℚ) := by          unfold d          unfold JohnsonBound.d          unfold d_weak          have min_dist := min_dist_le_d h_B2_not_one          have subset_inf_ineq :              sInf { d | ∃ u ∈ B, ∃ v ∈ B, u ≠ v ∧ Δ₀(u, v) = d } ≤              sInf { d |              ∃ u ∈ (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)),              ∃ v_1 ∈ (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)),              u ≠ v_1 ∧ Δ₀(u, v_1) = d } := by              have subset : { d |                          ∃ u ∈ (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)),                          ∃ v_1 ∈ (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)),                          u ≠ v_1 ∧ Δ₀(u, v_1) = d }                          ⊆ { d | ∃ u ∈ B, ∃ v ∈ B, u ≠ v ∧ Δ₀(u, v) = d } := by                intro d ⟨u, hu_in, v_1, hv_in, hne, heq⟩                exact                  ⟨u, by                    simp only [mem_inter, mem_filter, mem_univ, true_and] at hu_in; exact hu_in.1,                  v_1, by                    simp only [mem_inter, mem_filter, mem_univ, true_and] at hv_in; exact hv_in.1,                  hne, heq⟩              gcongr              obtain ⟨u, hu, v_1, hv_1, hne⟩ := one_lt_card.mp h_B2_not_one              use Δ₀(u, v_1)              exact ⟨u, hu, v_1, hv_1, hne, rfl⟩          calc ↑d_weak              = ↑(sInf { d | ∃ u ∈ B, ∃ v ∈ B, ¬u = v ∧ Δ₀(u, v) = d }) := by rfl            _ ≤ ↑(sInf { d |              ∃ u ∈ (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)),              ∃ v_1 ∈ (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)),              u ≠ v_1 ∧ Δ₀(u, v_1) = d }) := by exact_mod_cast subset_inf_ineq            _ ≤ JohnsonBound.d (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)) :=              by exact_mod_cast min_dist      have bound : (↑frac)⁻¹ * (1 - √(1 - ↑frac * ↑d_weak / ↑n))          ≤ (↑frac)⁻¹ * (1 - √(1 - ↑frac * ↑d / ↑n)) := by        have ineq1 : (↑d_weak / ↑n) ≤ (d / ↑n) := by          rw [← mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr h_n_pos)]          field_simp          exact d_subset        have ineq2 : frac * (d_weak / n) ≤ frac * (d / n) :=          mod_cast (mul_le_mul_iff_of_pos_left h_frac_pos).mpr ineq1        have ineq3' : (1 : ℝ) - frac * d / n ≤ (1 : ℝ) - frac * d_weak / n := by          norm_cast; grind        have ineq4 : √(1 - ↑frac * ↑d / ↑n) ≤ √(1 - ↑frac * ↑d_weak / ↑n) :=          sqrt_le_sqrt ineq3'        have ineq5 :            (1 - √(1 - ↑frac * ↑d_weak / ↑n)) ≤ (1 - √(1 - ↑frac * ↑d / ↑n)) := by linarith        simp_all      have h_J_cond_weak' : ↑e / ↑n < 1 / (↑frac) * (1 - √(1 - frac * (d_weak / ↑n))) := by        unfold frac        unfold q        unfold d_weak        push_cast        rw [one_div_div]        exact h_J_cond_weak      field_simp      field_simp at h_J_cond_weak'      field_simp at bound      nlinarith [mul_le_mul_of_nonneg_left bound (Nat.cast_nonneg n)]    have err_n : (↑e_1 / ↑n : ℝ) ≤ (↑e / ↑n : ℝ) := by      apply div_le_div_of_nonneg_right _ (Nat.cast_nonneg n)      exact_mod_cast e_ball_le_radius v e        (by simpa using show 0 < (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)).card by omega)    have j_fun_bound_e1 : (↑e_1 / ↑n : ℝ) < (1 / ↑frac * (1 - √(1 - ↑frac * ↑d / ↑n))) :=      lt_of_le_of_lt err_n j_fun_bound    have rearrange_jboundw_e1 : √(1 - ↑frac * ↑d / ↑n) < 1 - frac * e_1 / ↑n := by      have : frac * e_1 / ↑n < 1 - √(1 - frac * d / ↑n) := by        calc ↑frac * ↑e_1 / ↑n            = ↑frac * (↑e_1 / ↑n) := by ring          _ < ↑frac * (1 / ↑frac * (1 - √(1 - ↑frac * ↑d / ↑n))) := by            simp_all only [Rat.cast_div, Rat.cast_natCast, Rat.cast_sub, Rat.cast_one, sub_nonneg,              Nat.cast_pos, Finset.card_pos, gt_iff_lt, zero_lt_card, div_pos_iff_of_pos_left,              sub_pos, Nat.one_lt_cast, one_div, inv_div, mul_lt_mul_iff_right₀, frac, q, d, e_1]          _ = 1 - √(1 - ↑frac * ↑d / ↑n) := by            grind only [= division_by_conjugate, = sqrt_one]      grind only    have h_esqrtpos : (0 : ℝ) ≤ 1 - frac * e_1 / ↑n := by      have : (0 : ℝ) ≤ √(1 - ↑frac * ↑d / ↑n) := by        simp_all only [Rat.cast_div, Rat.cast_natCast, Rat.cast_sub, Rat.cast_one, sub_nonneg,          Nat.cast_pos, Finset.card_pos, gt_iff_lt, zero_lt_card, div_pos_iff_of_pos_left,          sub_pos, Nat.one_lt_cast, one_div, inv_div, sqrt_nonneg, frac, q, d, e_1]      grind only    suffices recast_main_goal : (1 - frac * d / ↑n : ℝ) < (1 - frac * e_1 / ↑n) ^ 2 by      exact_mod_cast recast_main_goal    suffices roots : √(1 - frac * d / ↑n) < 1 - frac * e_1 / ↑n by      rw [← sqrt_lt h_dsqrt_pos h_esqrtpos]      exact_mod_cast roots    exact rearrange_jboundw_e1  · have strict_neg : 1 - ↑frac * ↑d / ↑n < (0 : ℚ) := by      have : ¬(0 : ℚ) ≤ 1 - frac * d / ↑n := by exact_mod_cast h_dsqrt_pos      rw [Rat.not_le] at this      exact this    calc 1 - ↑frac * ↑d / ↑n < (0 : ℚ) := strict_neg      _ ≤ (1 - ↑frac * ↑e_1 / ↑n) ^ 2 := by exact_mod_cast sq_nonneg (1 - frac * ↑e_1 / ↑n)