awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₂ : ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
Tactic: calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₂ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₃ : ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
  ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
Tactic: calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₂ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₃ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₄ : ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
Tactic: calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₂ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₃ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₄ : ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₅ : ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4
Tactic: calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₂ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₃ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₄ : ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₅ : ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₆ : 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4 ≤ 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4
Tactic: calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₂ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₃ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₄ : ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₅ : ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4
_₆ : 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4 ≤ 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₇ : 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4 = 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3
Tactic: calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₂ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₃ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₄ : ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₅ : ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4
_₆ : 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4 ≤ 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4
_₇ : 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4 = 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₈ : 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3 = 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
Tactic: calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
x : ℝ
h : x > 0
⊢ LT.lt (α := ℝ) (-3) (-(↑(finrank ℤ ↥L.lattice) : ℝ))
have simp : LT.lt (α := ℝ) 2 3
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦
      if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    ℘[L - l₀]
have refine : ∀ (r : ℝ) (hr : r > 0),
  ∀ b ≥ 2 * r,
    ∀ (x : ℂ),
      ‖x‖ < r →
        ∀ (l : ↥L.lattice),
          ‖(↑l : ℂ)‖ = b →
            ‖if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2‖ ≤
              (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l
Tactic: refine L.hasSumLocallyUniformly_aux (u := (10 * · * ‖·‖ ^ (-3 : ℝ))) _
    (fun _ _ ↦ (ZLattice.summable_norm_rpow _ _ (by simp; norm_num)).mul_left _) fun r hr ↦
    Filter.eventually_atTop.mpr ⟨2 * r, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
⊢ ‖if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2‖ ≤
    (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l
have pos : (↑l : ℂ) = l₀ → norm (E := ℂ) 0 ≤ (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
pos : (↑l : ℂ) = l₀ → norm (E := ℂ) 0 ≤ (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l
⊢ ‖if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2‖ ≤
    (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l
have neg : ¬(↑l : ℂ) = l₀ →
  ‖1 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2‖ ≤
    (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
⊢ DifferentiableOn ℂ ℘[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have refine : ∀ (s : Finset ↥L.lattice) (i : ↥L.lattice) (hi : i ∈ s),
  DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: refine (L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSumLocallyUniformlyOn.differentiableOn
    (.of_forall fun s ↦ .fun_sum fun i hi ↦ ?_) L.isOpen_compl_lattice_diff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have pos : (↑i : ℂ) = l₀ → DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
pos : (↑i : ℂ) = l₀ → DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have neg : ¬(↑i : ℂ) = l₀ →
  DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
⊢ Eq (α := ℂ)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (-z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = -l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
have rw : Eq (α := ℂ)
  (∑' (c : ↥L.lattice),
    if (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
    else
      1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 2 -
        1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) 2)
  (∑' (l : ↥L.lattice),
    if (↑l : ℂ) = -l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
Tactic: rw [← (Equiv.neg L.lattice).tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
⊢ Eq (α := ℂ)
    (∑' (c : ↥L.lattice),
      if (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
      else
        1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 2 -
          1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) 2)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = -l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
have h : ∀ (l : ↥L.lattice), (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀
Tactic: congr! 3 with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
h : ∀ (l : ↥L.lattice), (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀
⊢ Eq (α := ℂ)
    (∑' (c : ↥L.lattice),
      if (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
      else
        1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 2 -
          1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) 2)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = -l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
have h₁ : ∀ (l : ↥L.lattice),
  ¬(↑l : ℂ) = -l₀ →
    1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ)) 2 -
        1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) 2 =
      1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
Tactic: congr! 3 with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
h : ¬(↑l : ℂ) = -l₀
⊢ 1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ)) 2 -
      1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) 2 =
    1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
have h : HPow.hPow (β := ℕ) (-z + (↑l : ℂ)) 2 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) = ℘[L] z
have trans : ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) =
  ℘[L - (↑l₀ : ℂ)] z +
    ∑' (i : ↥L.lattice),
      if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 else 0
Tactic: trans ℘[L - l₀] z + ∑' i : L.lattice, if i = l₀.1 then (1 / (z - l₀.1) ^ 2 - 1 / l₀.1 ^ 2) else 0