awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)
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)
⊢ 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 : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i

Premises used: HSub.hSub, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)
    (∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i)

Tactic:
simp only [weierstrassPExceptSummand, ite_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, PeriodPair.weierstrassPExceptSummand, ite_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
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)
⊢ 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:
simp_rw [coeff_weierstrassPExceptSeries, ← tsum_mul_right]

Premises used: PeriodPair.coeff_weierstrassPExceptSeries, tsum_mul_right
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
h :
  Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
⊢ 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:
apply Summable.tsum_comm

Premises used: Summable.tsum_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

Tactic:
L.summable_weierstrassPExceptSummand l₀ z x hx

Premises used: PeriodPair.summable_weierstrassPExceptSummand
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

Tactic:
exact L.summable_weierstrassPExceptSummand l₀ z x hx

Premises used: PeriodPair.summable_weierstrassPExceptSummand
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)

Tactic:
(Summable.hasSum_iff ?_).mpr (L.weierstrassPExcept_eq_tsum l₀ z x hx).symm

Premises used: Iff.mpr, PeriodPair.weierstrassPExcept_eq_tsum, Summable.hasSum_iff, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
refine : Summable (α := ℂ) fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
⊢ HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i) (℘[L - l₀] z)

Tactic:
refine (Summable.hasSum_iff ?_).mpr (L.weierstrassPExcept_eq_tsum l₀ z x hx).symm

Premises used: Iff.mpr, PeriodPair.weierstrassPExcept_eq_tsum, Summable.hasSum_iff, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
simp_rw : Summable (α := ℂ) fun (i : ℕ) ↦ ∑' (x_1 : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i x_1 * (z - x) ^ i
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
simp_rw [coeff_weierstrassPExceptSeries, ← tsum_mul_right]

Premises used: PeriodPair.coeff_weierstrassPExceptSeries, tsum_mul_right
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ ∑' (x_1 : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i x_1 * (z - x) ^ i

Tactic:
(L.summable_weierstrassPExceptSummand l₀ z x hx).prod

Premises used: Summable.prod, PeriodPair.summable_weierstrassPExceptSummand
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ ∑' (x_1 : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i x_1 * (z - x) ^ i

Tactic:
exact (L.summable_weierstrassPExceptSummand l₀ z x hx).prod

Premises used: Summable.prod, PeriodPair.summable_weierstrassPExceptSummand
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)
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))
⊢ HasFPowerSeriesOnBall ℘[L - l₀] (L.weierstrassPExceptSeries l₀ x) x (↑r : ENNReal)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
r_le : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * (↑r : ℝ) ^ n) atTop (𝓝 0)
⊢ (↑r : ENNReal) ≤ (L.weierstrassPExceptSeries l₀ x).radius

Tactic:
apply FormalMultilinearSeries.le_radius_of_tendsto (l := 0)

Premises used: FormalMultilinearSeries.le_radius_of_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ Tendsto (α := ℕ)
    ((fun (a : ℂ) ↦ ‖a‖) ∘ fun (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + (↑(↑r : ℝ) : ℂ) - x) ^ i)
    atTop (𝓝 (norm (E := ℂ) 0))

Tactic:
tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero

Premises used: Summable.tendsto_atTop_zero, Complex.ofReal, HasSum.summable, HAdd.hAdd, tendsto_norm, PeriodPair.weierstrassPExceptSeries_hasSum, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
r_le : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖x + (↑(↑r : ℝ) : ℂ) - x‖ < ‖(↑l : ℂ) - x‖
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * (↑r : ℝ) ^ n) atTop (𝓝 0)

Tactic:
convert!
      tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero using
      2 with i

Premises used: Summable.tendsto_atTop_zero, Complex.ofReal, HasSum.summable, HAdd.hAdd, tendsto_norm, PeriodPair.weierstrassPExceptSeries_hasSum, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
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:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ 0 = norm (E := ℂ) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
l : ↥L.lattice
hl : (↑l : ℂ) ≠ l₀
⊢ ‖x + (↑(↑r : ℝ) : ℂ) - x‖ < ‖(↑l : ℂ) - x‖

Tactic:
simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm]
        using Set.subset_compl_comm.mp hr ⟨l.2, hl⟩

Premises used: Set.subset_compl_comm, mem_closedBall_iff_norm, And.intro, Iff.mp, Metric.mem_closedBall, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ 0 < (↑r : ENNReal)

Tactic:
ENNReal.coe_pos.mpr hr0

Premises used: Iff.mpr, ENNReal.coe_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ 0 < (↑r : ENNReal)

Tactic:
exact ENNReal.coe_pos.mpr hr0

Premises used: Iff.mpr, ENNReal.coe_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
⊢ ‖z‖ < (↑r : ℝ)

Tactic:
simpa using hz
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
⊢ ‖z‖ < (↑r : ℝ)

Tactic:
replace hz : ‖z‖ < r := by simpa using hz
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < (↑r : ℝ)
⊢ ∀ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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))
⊢ ∀ (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

Premises used: add_sub_cancel_left
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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))
l : ↥L.lattice
hl : (↑l : ℂ) ≠ l₀
⊢ (↑r : ℝ) < ‖(↑l : ℂ) - x‖

Tactic:
simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm] using
        Set.subset_compl_comm.mp hr ⟨l.2, hl⟩

Premises used: Set.subset_compl_comm, mem_closedBall_iff_norm, And.intro, Iff.mp, Metric.mem_closedBall, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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))
⊢ ∀ (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⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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 (i : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))

Tactic:
this (fun l hl ↦ hz.trans (A l hl))

Premises used: LT.lt.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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‖
h :
  ∀ (i : ℕ),
    ((L.weierstrassPExceptSeries l₀ x i : (a : (i : Fin i) → ℂ) → ℂ) fun (x : Fin i) ↦ z) =
      (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i
⊢ HasSum (fun (n : ℕ) ↦ (L.weierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ z)
    (℘[L - l₀] (x + z))

Tactic:
convert! this (fun l hl ↦ hz.trans (A l hl)) with i

Premises used: LT.lt.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
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
h₃ 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
⊢ ((L.weierstrassPExceptSeries l₀ x i : (a : (i : Fin i) → ℂ) → ℂ) fun (x : Fin i) ↦ z) =
    (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i

Tactic:
rw [weierstrassPExceptSeries, FormalMultilinearSeries.ofScalars_apply_eq,
      FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul]

Premises used: FormalMultilinearSeries.ofScalars_apply_eq, FormalMultilinearSeries.coeff_ofScalars, PeriodPair.weierstrassPExceptSeries, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
obtain :
  ∀ (r : ℝ) (h₁ : 0 < r) (h₂ : Metric.closedBall l r ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ),
    HasFPowerSeriesAt (𝕜 := ℂ) ℘[L - l]
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow l (i + 2))
      l
⊢ HasFPowerSeriesAt (𝕜 := ℂ) ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      if i = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow l (i + 2))
    l

Tactic:
obtain ⟨r, h₁, h₂⟩ := Metric.nhds_basis_closedBall.mem_iff.mp
    (L.compl_lattice_diff_singleton_mem_nhds l)

Premises used: Filter.HasBasis.mem_iff, PeriodPair.compl_lattice_diff_singleton_mem_nhds, Iff.mp, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ
⊢ 0 ≤ r

Tactic:
h₁.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ
lift :
  ∀ (r : NNReal) (h₁ : 0 < (↑r : ℝ)) (h₂ : Metric.closedBall l (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ),
    HasFPowerSeriesAt (𝕜 := ℂ) ℘[L - l]
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow l (i + 2))
      l
⊢ HasFPowerSeriesAt (𝕜 := ℂ) ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      if i = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow l (i + 2))
    l

Tactic:
lift r to NNReal using h₁.le

Premises used: LT.lt.le, NNReal
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
r : NNReal
h₁ : 0 < (↑r : ℝ)
h₂ : Metric.closedBall l (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ
⊢ HasFPowerSeriesAt (𝕜 := ℂ) ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      if i = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow l (i + 2))
    l

Tactic:
simpa [weierstrassPExceptSeries] using
    (L.hasFPowerSeriesOnBall_weierstrassPExcept l l r h₁ h₂).hasFPowerSeriesAt

Premises used: PeriodPair.weierstrassPExceptSeries, PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept, HasFPowerSeriesOnBall.hasFPowerSeriesAt
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ AnalyticOnNhd ℂ ℘[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
(L.differentiableOn_weierstrassPExcept l₀).analyticOnNhd L.isOpen_compl_lattice_diff

Premises used: PeriodPair.isOpen_compl_lattice_diff, DifferentiableOn.analyticOnNhd, PeriodPair.differentiableOn_weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ l₀ ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ Ne (α := ℂ) (↑n ! : ℂ) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
rw :
  iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
    (if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)) / (↑n ! : ℂ)
⊢ iteratedDeriv n ℘[L - l] l = if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)

Tactic:
rw [← div_mul_cancel₀ (a := iteratedDeriv _ _ _) (b := ↑n !) (by simp),
    ← eq_div_iff_mul_eq (by simp)]

Premises used: div_mul_cancel₀, eq_div_iff_mul_eq, iteratedDeriv
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
trans :
  iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
    if n = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * L.sumInvPow l (n + 2)
trans₁ :
  (if n = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * L.sumInvPow l (n + 2)) =
    (if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)) / (↑n ! : ℂ)
⊢ iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
    (if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)) / (↑n ! : ℂ)

Tactic:
trans if n = 0 then ℘[L - l] l else (n + 1) * L.sumInvPow l (n + 2)

Premises used: HAdd.hAdd, OfNat.ofNat, PeriodPair.sumInvPow, PeriodPair.weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
    if n = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * L.sumInvPow l (n + 2)

Tactic:
simpa using congr($((L.analyticAt_weierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_weierstrassPExcept l)).coeff n)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
zero :
  (if Eq (α := ℕ) 0 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * L.sumInvPow l (HAdd.hAdd (α := ℕ) 0 2)) =
    (if Eq (α := ℕ) 0 0 then ℘[L - l] l
      else (↑(HAdd.hAdd (α := ℕ) 0 1)! : ℂ) * L.sumInvPow l (HAdd.hAdd (α := ℕ) 0 2)) /
      (↑0! : ℂ)
succ :
  ∀ (n : ℕ),
    (if n + 1 = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1 * L.sumInvPow l (n + 1 + 2)) =
      (if n + 1 = 0 then ℘[L - l] l else (↑(n + 1 + 1)! : ℂ) * L.sumInvPow l (n + 1 + 2)) / (↑(n + 1)! : ℂ)
⊢ (if n = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * L.sumInvPow l (n + 2)) =
    (if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)) / (↑n ! : ℂ)

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
⊢ (if Eq (α := ℕ) 0 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * L.sumInvPow l (HAdd.hAdd (α := ℕ) 0 2)) =
    (if Eq (α := ℕ) 0 0 then ℘[L - l] l
      else (↑(HAdd.hAdd (α := ℕ) 0 1)! : ℂ) * L.sumInvPow l (HAdd.hAdd (α := ℕ) 0 2)) /
      (↑0! : ℂ)

Tactic:
simp [Nat.factorial_succ]

Premises used: Nat.factorial_succ