awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[L - (↑l₀ : ℂ)] z = ℘'[L] z + 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3
have rw : ℘'[L - (↑l₀ : ℂ)] z =
  ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 + 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3
Tactic: rw [← L.derivWeierstrassPExcept_sub l₀, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
rw :
  ℘'[L - (↑l₀ : ℂ)] z =
    ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 + 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3
⊢ ℘'[L - (↑l₀ : ℂ)] z = ℘'[L] z + 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3
have rw₁ : ℘'[L - (↑l₀ : ℂ)] z = ℘'[L - (↑l₀ : ℂ)] z
Tactic: rw [← L.derivWeierstrassPExcept_sub l₀, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ Eq (α := (z : ℂ) → ℂ)
    (fun (z : ℂ) ↦ ∑' (l : ↥L.lattice), if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
    fun (z : ℂ) ↦ -∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
have simp_rw : Eq (α := (z : ℂ) → ℂ)
  (fun (z : ℂ) ↦ ∑' (l : ↥L.lattice), if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
  fun (z : ℂ) ↦ ∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
Tactic: simp_rw [← tsum_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ Eq (α := (z : ℂ) → ℂ)
    (fun (z : ℂ) ↦ ∑' (l : ↥L.lattice), if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
    fun (z : ℂ) ↦ ∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
have h : ∀ (z : ℂ) (l : ↥L.lattice),
  (if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) = -(2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
Tactic: congr! 3 with z l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
z : ℂ
l : ↥L.lattice
⊢ (if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) = -(2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
have this : (↑l : ℂ) ≠ l₀
Tactic: have : l.1 ≠ l₀ := by rintro rfl; simp at hl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) ↦ -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) ℘'[L]
have h : ∀ (l : ↥L.lattice) (z : ℂ),
  -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3 = if (↑l : ℂ) = L.ω₁ / 2 then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
Tactic: convert! L.hasSumLocallyUniformly_derivWeierstrassPExcept (L.ω₁ / 2) using 3 with l z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
h :
  ∀ (l : ↥L.lattice) (z : ℂ),
    -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3 =
      if (↑l : ℂ) = L.ω₁ / 2 then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
⊢ HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) ↦ -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) ℘'[L]
have h₁ : ℘'[L] = ℘'[L - L.ω₁ / 2]
Tactic: convert! L.hasSumLocallyUniformly_derivWeierstrassPExcept (L.ω₁ / 2) using 3 with l z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3 = if (↑l : ℂ) = L.ω₁ / 2 then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
have h : ¬(↑l : ℂ) = L.ω₁ / 2
Tactic: rw [if_neg, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ ℘'[L] = ℘'[L - L.ω₁ / 2]
have h : ℘'[L] = ℘'[L]
Tactic: rw [L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ DifferentiableOn ℂ ℘'[L] (↑L.lattice : Set ℂ)ᶜ
have rw : DifferentiableOn ℂ ℘'[L - L.ω₁ / 2] (↑L.lattice : Set ℂ)ᶜ
Tactic: rw [← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
⊢ Eq (α := ℂ) (-∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (-z - (↑l : ℂ)) 3)
    (- -∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
have rw : Eq (α := ℂ)
  (-∑' (c : ↥L.lattice),
      2 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
  (- -∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
Tactic: rw [← (Equiv.neg L.lattice).tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
⊢ Eq (α := ℂ)
    (-∑' (c : ↥L.lattice),
        2 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
    (- -∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
have simp : Eq (α := ℂ) (∑' (b : ↥L.lattice), 2 / -HPow.hPow (β := ℕ) ((↑b : ℂ) - z) 3)
  (∑' (b : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
Tactic: simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub, neg_neg,
    ← div_neg, ← tsum_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
⊢ Eq (α := ℂ) (∑' (b : ↥L.lattice), 2 / -HPow.hPow (β := ℕ) ((↑b : ℂ) - z) 3)
    (∑' (b : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
have h : ∀ (l : ↥L.lattice), -HPow.hPow (β := ℕ) ((↑l : ℂ) - z) 3 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
Tactic: congr! with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ Eq (α := ℂ) (-∑' (l_1 : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l_1 : ℂ)) 3)
    (-∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
have rw : Eq (α := ℂ)
  (-∑' (c : ↥L.lattice),
      2 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑((Equiv.addRight l : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
  (-∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
Tactic: rw [← (Equiv.addRight l).tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ ℘'[L] 0 = 0
have rw : ℘'[L] 0 = -℘'[L] 0
Tactic: rw [← CharZero.eq_neg_self_iff, ← L.derivWeierstrassP_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
rw : ℘'[L] 0 = -℘'[L] 0
⊢ ℘'[L] 0 = 0
have rw₁ : ℘'[L] 0 = ℘'[L] (-0)
Tactic: rw [← CharZero.eq_neg_self_iff, ← L.derivWeierstrassP_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
rw : ℘'[L] 0 = -℘'[L] 0
rw₁ : ℘'[L] 0 = ℘'[L] (-0)
⊢ ℘'[L] 0 = 0
have rw₂ : ℘'[L] 0 = ℘'[L] 0
Tactic: rw [← CharZero.eq_neg_self_iff, ← L.derivWeierstrassP_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ↥L.lattice
⊢ ℘'[L] (↑l : ℂ) = 0
have rw : ℘'[L] (0 + (↑l : ℂ)) = 0
Tactic: rw [← zero_add l.1, L.derivWeierstrassP_add_coe, L.derivWeierstrassP_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ↥L.lattice
rw : ℘'[L] (0 + (↑l : ℂ)) = 0
⊢ ℘'[L] (↑l : ℂ) = 0
have rw₁ : ℘'[L] 0 = 0
Tactic: rw [← zero_add l.1, L.derivWeierstrassP_add_coe, L.derivWeierstrassP_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ↥L.lattice
rw : ℘'[L] (0 + (↑l : ℂ)) = 0
rw₁ : ℘'[L] 0 = 0
⊢ ℘'[L] (↑l : ℂ) = 0
have rw₂ : Eq (α := ℂ) 0 0
Tactic: rw [← zero_add l.1, L.derivWeierstrassP_add_coe, L.derivWeierstrassP_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘'[L] (z - (↑l : ℂ)) = ℘'[L] z
have rw : ℘'[L] (z - (↑l : ℂ) + (↑l : ℂ)) = ℘'[L] z
Tactic: rw [← L.derivWeierstrassP_add_coe _ l, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
rw : ℘'[L] (z - (↑l : ℂ) + (↑l : ℂ)) = ℘'[L] z
⊢ ℘'[L] (z - (↑l : ℂ)) = ℘'[L] z
have rw₁ : ℘'[L] z = ℘'[L] z
Tactic: rw [← L.derivWeierstrassP_add_coe _ l, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ deriv ℘[L] = ℘'[L]
have h : ∀ (x : ℂ), deriv ℘[L] x = ℘'[L] x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
⊢ deriv ℘[L] x = ℘'[L] x
have pos : ∀ (hx : x ∈ L.lattice), deriv ℘[L] x = ℘'[L] x
Tactic: by_cases hx : x ∈ L.lattice
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
pos : ∀ (hx : x ∈ L.lattice), deriv ℘[L] x = ℘'[L] x
⊢ deriv ℘[L] x = ℘'[L] x
have neg : ∀ (hx : x ∉ L.lattice), deriv ℘[L] x = ℘'[L] x
Tactic: by_cases hx : x ∈ L.lattice
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ deriv ℘[L] x = ℘'[L] x
have pos : ¬DifferentiableAt ℂ ℘[L] x
Tactic: rw [deriv_zero_of_not_differentiableAt, L.derivWeierstrassP_coe ⟨x, hx⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ deriv ℘[L] x = ℘'[L] x
have neg : deriv ℘[L - L.ω₁ / 2] x = ℘'[L] x
Tactic: rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      ← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L.ω₁ / 2) (x := x) (by simp [hx])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
neg : deriv ℘[L - L.ω₁ / 2] x = ℘'[L] x
⊢ deriv ℘[L] x = ℘'[L] x
have neg₁ : deriv ℘[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x
Tactic: rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      ← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L.ω₁ / 2) (x := x) (by simp [hx])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
neg : deriv ℘[L - L.ω₁ / 2] x = ℘'[L] x
neg₁ : deriv ℘[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x
⊢ deriv ℘[L] x = ℘'[L] x
have neg₂ : ℘'[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x
Tactic: rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      ← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L.ω₁ / 2) (x := x) (by simp [hx])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
⊢ HasSum (fun (l : ↥L.lattice) ↦ (((↑l : ℂ) - x) ^ r)⁻¹) (L.sumInvPow x r)
have refine : ∀ (l : ↥L.lattice), ‖(((↑l : ℂ) - x) ^ r)⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
Tactic: refine Summable.hasSum (.of_norm_bounded (ZLattice.summable_norm_sub_zpow _
    (-r) (by simpa) x) fun l ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
⊢ ‖(((↑l : ℂ) - x) ^ r)⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
have rw : ‖(HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑r : ℤ))⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
Tactic: rw [← zpow_natCast, ← zpow_neg, ← norm_zpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
rw : ‖(HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑r : ℤ))⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
⊢ ‖(((↑l : ℂ) - x) ^ r)⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
have rw₁ : ‖HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑r : ℤ))‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
Tactic: rw [← zpow_natCast, ← zpow_neg, ← norm_zpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
rw : ‖(HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑r : ℤ))⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
rw₁ : ‖HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑r : ℤ))‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
⊢ ‖(((↑l : ℂ) - x) ^ r)⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
have rw₂ : ‖HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑r : ℤ))‖ ≤ ‖HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑r : ℤ))‖
Tactic: rw [← zpow_natCast, ← zpow_neg, ← norm_zpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x
        else
          HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 *
            (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0))
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
have pos : ∀ (hl₀ : l₀ ∈ L.lattice),
  FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
Tactic: split_ifs with hl₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
pos :
  ∀ (hl₀ : l₀ ∈ L.lattice),
    FormalMultilinearSeries.coeff
        (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
          if i = 0 then ℘[L - l₀] x
          else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
        (i + 1) =
      ∑' (l : ↥L.lattice),
        if (↑l : ℂ) = l₀ then 0
        else
          HSub.hSub (β := ℂ)
            (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x
        else
          HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 *
            (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0))
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
have neg : ∀ (hl₀ : l₀ ∉ L.lattice),
  FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - 0))
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
Tactic: split_ifs with hl₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
have trans : FormalMultilinearSeries.coeff
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
    (i + 1) =
  HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
    (L.sumInvPow x (i + 3) -
      ∑' (l : ↥L.lattice),
        if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
        else 0)
Tactic: trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
trans :
  FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (i + 1) =
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0)
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
have trans₁ : HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
    (L.sumInvPow x (i + 3) -
      ∑' (l : ↥L.lattice),
        if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
        else 0) =
  ∑' (l : ↥L.lattice),
    if (↑l : ℂ) = l₀ then 0
    else
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
        (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
Tactic: trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (i + 1) =
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0)
have rw : (if i + 1 = 0 then ℘[L - l₀] x
  else HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
  HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ (i + 3))⁻¹)
Tactic: rw [FormalMultilinearSeries.coeff_ofScalars, tsum_ite_eq, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ 2 < i + 3
have linarith : i + 3 ≤ 2 → -1 + HSub.hSub (α := ℤ) 0 (↑i : ℤ) + (HAdd.hAdd (α := ℤ) (↑i : ℤ) 3 - 2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
have rw : Eq (α := ℂ)
  (∑' (x_1 : ↥L.lattice),
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      ((((↑x_1 : ℂ) - x) ^ (i + 3))⁻¹ -
        if x_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
        else 0))
  (∑' (l : ↥L.lattice),
    if (↑l : ℂ) = l₀ then 0
    else
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
        (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ))
Tactic: rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
rw :
  Eq (α := ℂ)
    (∑' (x_1 : ↥L.lattice),
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
        ((((↑x_1 : ℂ) - x) ^ (i + 3))⁻¹ -
          if x_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then
            HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0))
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ))
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0) =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
have rw₁ : Summable (α := ℂ) fun (l : ↥L.lattice) ↦
  if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ)) else 0
Tactic: rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Eq (α := ℂ)
    (∑' (x_1 : ↥L.lattice),
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
        ((((↑x_1 : ℂ) - x) ^ (i + 3))⁻¹ -
          if x_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then
            HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0))
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ))
have simp_rw : Eq (α := ℂ)
  (∑' (x_1 : ↥L.lattice),
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      ((((↑x_1 : ℂ) - x) ^ (i + 3))⁻¹ - if (↑x_1 : ℂ) = l₀ then (HPow.hPow (β := ℤ) (l₀ - x) (↑(i + 3) : ℤ))⁻¹ else 0))
  (∑' (l : ↥L.lattice),
    if (↑l : ℂ) = l₀ then 0
    else HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑(i + 1 + 2) : ℤ))⁻¹ - 0 i)
Tactic: simp_rw [Subtype.ext_iff, zpow_neg]