Sqrt le J

lemma sqrt_le_J {q δ : ℚ} (hq : q > 1) (hx0 : 0 ≤ δ) (hx1 : δ ≤ 1)    (hqx : q / (q - 1) * δ ≤ 1) :    1 - √(1 - δ) ≤ J q δ := by  unfold J  set frac := q / (q - 1) with hfrac  have hfrac_ge : frac ≥ 1 := by    rw [hfrac, ge_iff_le, one_le_div] <;> grind  have hx' : 1 - δ ≥ 0 := by grind only  have hfracx' : 1 - frac * δ ≥ 0 := by grind only  suffices 1 - √(1 - δ) ≤ (1 / frac) * (1 - √(1 - frac * δ)) by grind only  field_simp  norm_cast  by_cases hδ : δ = 0  · simp [hδ]  · have hδ_pos : (0 : ℚ) < δ := lt_of_le_of_ne hx0 (Ne.symm hδ)    have hfracx'2 : 1 - δ * frac ≥ 0 := by linarith [mul_comm frac δ]    rw [division_by_conjugate (b := ↑(1 - δ)) (by exact_mod_cast hx') (by positivity)]    rw [division_by_conjugate (b := ↑(1 - δ * frac))        (by exact_mod_cast hfracx'2) (by positivity)]    simp only [one_pow]    push_cast    rw [show (1 : ℝ) - (1 - (δ : ℝ)) = δ from by ring,        show (1 : ℝ) - (1 - (δ : ℝ) * (frac : ℝ)) = δ * frac from by ring,        div_mul_eq_mul_div]    have hsqrt_le : √(1 - ↑δ * ↑frac) ≤ √(1 - ↑δ) := by      apply sqrt_le_sqrt      nlinarith [show (1 : ℝ) ≤ ↑frac from by exact_mod_cast hfrac_ge,                 show (0 : ℝ) ≤ ↑δ from by exact_mod_cast hx0]    exact div_le_div_of_nonneg_left (by positivity) (by positivity) (by linarith)