Johnson e div ne J

lemma johnson_e_div_ne_J {n d e : ℕ} {q : ℚ}    (hn_pos : 0 < n) (hd_pos : 0 < d) (hq : 1 < q)    (h_muln : ((e : ℚ) / n : ℝ) ≤ 1 - ((1 - (d : ℚ) / n) : ℝ).sqrt)    (h_J_bound : 1 - ((1 - (d : ℚ) / n) : ℝ).sqrt ≤ J' q (d / n))    (hqx : q / (q - 1) * (d / n) ≤ 1) :    ((e : ℚ) / n : ℝ) ≠ J' q (d / n) := by  intro h_eq  set δ := (d : ℚ) / n  set frac := q / (q - 1)  have h_frac_pos : 1 < frac := by rw [lt_div_iff₀] <;> linarith  have h_sqrt_eq : 1 - √(1 - δ) = (1 / frac) * (1 - √(1 - frac * δ)) := by    rw [show (1 : ℝ) - √(1 - (δ : ℝ)) = (e : ℚ) / n from      by        dsimp [δ] at h_muln h_J_bound h_eq ⊢        norm_cast at h_muln h_J_bound h_eq ⊢        exact le_antisymm (h_J_bound.trans_eq h_eq.symm) h_muln]    rw [h_eq]    rfl  have h_frac_eq : 1 - √(1 - δ) = δ / (1 + √(1 - δ)) ∧ (1 / frac) *      (1 - √(1 - frac * δ)) = δ / (1 + √(1 - frac * δ)) := by    constructor    · rw [eq_div_iff] <;> ring_nf <;> norm_num      · rw [sq_sqrt] <;> norm_num        exact_mod_cast div_le_one_of_le₀ (show (d : ℚ) ≤ n by          exact_mod_cast Nat.le_of_lt_succ <| by            rw [← @Nat.cast_lt ℚ]; push_cast            nlinarith [show (1 : ℚ) ≤ d by exact_mod_cast hd_pos,              show (1 : ℚ) ≤ n by exact_mod_cast hn_pos,              mul_div_cancel₀ (d : ℚ) (by positivity : (n : ℚ) ≠ 0),              div_mul_cancel₀ (q : ℚ) (by linarith : (q - 1 : ℚ) ≠ 0)]) (by positivity)      · positivity    · field_simp [frac] at *      linarith [mul_self_sqrt (show 0 ≤ 1 - (frac : ℝ) * δ by        exact sub_nonneg_of_le <| mod_cast hqx)]  have h_sqrt_eq' : √(1 - frac * δ) = √(1 - δ) := by grind  rw [sqrt_inj] at h_sqrt_eq' <;> norm_cast at * <;>    nlinarith [show (0 : ℚ) < δ by positivity]