awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ ℘[L - l₀] z = ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
have trans : ℘[L - l₀] z =
  ∑' (l : ↥L.lattice) (i : ℕ),
    if (↑l : ℂ) = l₀ then 0
    else
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
        (z - x) ^ i
Tactic: trans ∑' (l : L.lattice) (i : ℕ), if l.1 = l₀ then 0 else
      ((i + 1) * (l.1 - x) ^ (- ↑(i + 2) : ℤ) - i.casesOn (l.1 ^ (-2 : ℤ)) 0) * (z - x) ^ i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
trans :
  ℘[L - l₀] z =
    ∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i
⊢ ℘[L - l₀] z = ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
have trans₁ : Eq (α := ℂ)
  (∑' (l : ↥L.lattice) (i : ℕ),
    if (↑l : ℂ) = l₀ then 0
    else
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
        (z - x) ^ i)
  (∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i)
Tactic: trans ∑' (l : L.lattice) (i : ℕ), if l.1 = l₀ then 0 else
      ((i + 1) * (l.1 - x) ^ (- ↑(i + 2) : ℤ) - i.casesOn (l.1 ^ (-2 : ℤ)) 0) * (z - x) ^ i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Eq (α := ℂ)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    (∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i)
have e_f : ∀ (l : ↥L.lattice),
  (if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) =
    ∑' (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i
Tactic: congr 1 with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
l : ↥L.lattice
⊢ (if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) =
    ∑' (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i
have pos : ∀ (h : (↑l : ℂ) = l₀), Eq (α := ℂ) 0 (∑' (i : ℕ), 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
l : ↥L.lattice
pos : ∀ (h : (↑l : ℂ) = l₀), Eq (α := ℂ) 0 (∑' (i : ℕ), 0)
⊢ (if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) =
    ∑' (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i
have neg : ∀ (h : ¬(↑l : ℂ) = l₀),
  1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2 =
    ∑' (i : ℕ),
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
        (z - x) ^ i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Eq (α := ℂ)
    (∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i)
    (∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i)
have trans : Eq (α := ℂ)
  (∑' (l : ↥L.lattice) (i : ℕ),
    if (↑l : ℂ) = l₀ then 0
    else
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
        (z - x) ^ i)
  (∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i)
Tactic: trans ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
trans :
  Eq (α := ℂ)
    (∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i)
    (∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i)
⊢ Eq (α := ℂ)
    (∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i)
    (∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i)
have trans₁ : Eq (α := ℂ) (∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i)
  (∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i)
Tactic: trans ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Eq (α := ℂ) (∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i)
    (∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i)
have simp_rw : Eq (α := ℂ) (∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i)
  (∑' (i : ℕ) (x_1 : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i x_1 * (z - x) ^ i)
Tactic: simp_rw [coeff_weierstrassPExceptSeries, ← tsum_mul_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Eq (α := ℂ) (∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i)
    (∑' (i : ℕ) (x_1 : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i x_1 * (z - x) ^ i)
have h : Summable (α := ℂ) (β := ℕ × ↥L.lattice)
  (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
Tactic: apply Summable.tsum_comm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i) (℘[L - l₀] z)
have refine : Summable (α := ℂ) fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
Tactic: refine (Summable.hasSum_iff ?_).mpr (L.weierstrassPExcept_eq_tsum l₀ z x hx).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
have simp_rw : Summable (α := ℂ) fun (i : ℕ) ↦ ∑' (x_1 : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i x_1 * (z - x) ^ i
Tactic: simp_rw [coeff_weierstrassPExceptSeries, ← tsum_mul_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - l₀] (L.weierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
have r_le : (↑r : ENNReal) ≤ (L.weierstrassPExceptSeries l₀ x).radius
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
r_le : (↑r : ENNReal) ≤ (L.weierstrassPExceptSeries l₀ x).radius
⊢ HasFPowerSeriesOnBall ℘[L - l₀] (L.weierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
have r_pos : 0 < (↑r : ENNReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
r_le : (↑r : ENNReal) ≤ (L.weierstrassPExceptSeries l₀ x).radius
r_pos : 0 < (↑r : ENNReal)
⊢ HasFPowerSeriesOnBall ℘[L - l₀] (L.weierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
have hasSum : ∀ {y : ℂ},
  Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r : ENNReal)) y →
    HasSum (fun (n : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ y)
      (℘[L - l₀] (x + y))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ (↑r : ENNReal) ≤ (L.weierstrassPExceptSeries l₀ x).radius
have r_le : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * (↑r : ℝ) ^ n) atTop (𝓝 0)
Tactic: apply FormalMultilinearSeries.le_radius_of_tendsto (l := 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * (↑r : ℝ) ^ n) atTop (𝓝 0)
have h : ∀ (i : ℕ),
  ‖L.weierstrassPExceptSeries l₀ x i‖ * (↑r : ℝ) ^ i =
    ((fun (a : ℂ) ↦ ‖a‖) ∘ fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + (↑(↑r : ℝ) : ℂ) - x) ^ i) i
Tactic: convert!
      tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero using
      2 with i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
h :
  ∀ (i : ℕ),
    ‖L.weierstrassPExceptSeries l₀ x i‖ * (↑r : ℝ) ^ i =
      ((fun (a : ℂ) ↦ ‖a‖) ∘ fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + (↑(↑r : ℝ) : ℂ) - x) ^ i) i
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * (↑r : ℝ) ^ n) atTop (𝓝 0)
have h₁ : 0 = norm (E := ℂ) 0
Tactic: convert!
      tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero using
      2 with i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
h :
  ∀ (i : ℕ),
    ‖L.weierstrassPExceptSeries l₀ x i‖ * (↑r : ℝ) ^ i =
      ((fun (a : ℂ) ↦ ‖a‖) ∘ fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + (↑(↑r : ℝ) : ℂ) - x) ^ i) i
h₁ : 0 = norm (E := ℂ) 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * (↑r : ℝ) ^ n) atTop (𝓝 0)
have r_le : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖x + (↑(↑r : ℝ) : ℂ) - x‖ < ‖(↑l : ℂ) - x‖
Tactic: convert!
      tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero using
      2 with i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.eball 0 (↑r : ENNReal)) z
⊢ HasSum (fun (n : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ z)
    (℘[L - l₀] (x + z))
have hz₁ : ‖z‖ < (↑r : ℝ)
Tactic: replace hz : ‖z‖ < r := by simpa using hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
⊢ HasSum (fun (n : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ z)
    (℘[L - l₀] (x + z))
have this : ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖x + z - x‖ < ‖(↑l : ℂ) - x‖),
  HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + z - x) ^ i) (℘[L - l₀] (x + z))
Tactic: have := L.weierstrassPExceptSeries_hasSum l₀ (x + z) x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
this :
  ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖x + z - x‖ < ‖(↑l : ℂ) - x‖),
    HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + z - x) ^ i) (℘[L - l₀] (x + z))
⊢ HasSum (fun (n : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ z)
    (℘[L - l₀] (x + z))
have this₁ : ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z‖ < ‖(↑l : ℂ) - x‖),
  HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
Tactic: simp only [add_sub_cancel_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
this :
  ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z‖ < ‖(↑l : ℂ) - x‖),
    HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
⊢ HasSum (fun (n : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ z)
    (℘[L - l₀] (x + z))
have A : ∀ (l : ↥L.lattice) (hl : (↑l : ℂ) ≠ l₀), (↑r : ℝ) < ‖(↑l : ℂ) - x‖
Tactic: have A (l : ↥L.lattice) (hl : ↑l ≠ l₀) : r < ‖↑l - x‖ := by
      simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm] using
        Set.subset_compl_comm.mp hr ⟨l.2, hl⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
this :
  ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z‖ < ‖(↑l : ℂ) - x‖),
    HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice) (hl : (↑l : ℂ) ≠ l₀), (↑r : ℝ) < ‖(↑l : ℂ) - x‖
⊢ HasSum (fun (n : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ z)
    (℘[L - l₀] (x + z))
have h : ∀ (i : ℕ),
  ((L.weierstrassPExceptSeries l₀ x i : (a : (i : Fin i) → ℂ) → ℂ) fun (x : Fin i) ↦ z) =
    (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i
Tactic: convert! this (fun l hl ↦ hz.trans (A l hl)) with i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
this :
  ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z‖ < ‖(↑l : ℂ) - x‖),
    HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice) (hl : (↑l : ℂ) ≠ l₀), (↑r : ℝ) < ‖(↑l : ℂ) - x‖
i : ℕ
⊢ ((L.weierstrassPExceptSeries l₀ x i : (a : (i : Fin i) → ℂ) → ℂ) fun (x : Fin i) ↦ z) =
    (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i
have h : ((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 :
      (a : (i : Fin i) → ℂ) → ℂ)
    fun (x : Fin i) ↦ z) =
  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 *
    z ^ i
Tactic: rw [weierstrassPExceptSeries, FormalMultilinearSeries.ofScalars_apply_eq,
      FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
this :
  ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z‖ < ‖(↑l : ℂ) - x‖),
    HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice) (hl : (↑l : ℂ) ≠ l₀), (↑r : ℝ) < ‖(↑l : ℂ) - x‖
i : ℕ
h :
  ((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 :
        (a : (i : Fin i) → ℂ) → ℂ)
      fun (x : Fin i) ↦ z) =
    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 *
      z ^ i
⊢ ((L.weierstrassPExceptSeries l₀ x i : (a : (i : Fin i) → ℂ) → ℂ) fun (x : Fin i) ↦ z) =
    (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i
have h₁ : (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)) •
    z ^ 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 *
    z ^ i
Tactic: rw [weierstrassPExceptSeries, FormalMultilinearSeries.ofScalars_apply_eq,
      FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
this :
  ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z‖ < ‖(↑l : ℂ) - x‖),
    HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice) (hl : (↑l : ℂ) ≠ l₀), (↑r : ℝ) < ‖(↑l : ℂ) - x‖
i : ℕ
h :
  ((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 :
        (a : (i : Fin i) → ℂ) → ℂ)
      fun (x : Fin i) ↦ z) =
    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 *
      z ^ i
h₁ :
  (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)) •
      z ^ 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 *
      z ^ i
⊢ ((L.weierstrassPExceptSeries l₀ x i : (a : (i : Fin i) → ℂ) → ℂ) fun (x : Fin i) ↦ z) =
    (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i
have h₂ : (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)) •
    z ^ 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)) *
    z ^ i
Tactic: rw [weierstrassPExceptSeries, FormalMultilinearSeries.ofScalars_apply_eq,
      FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul]