awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
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
have 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
Tactic: obtain ⟨r, h₁, h₂⟩ := Metric.nhds_basis_closedBall.mem_iff.mp
    (L.compl_lattice_diff_singleton_mem_nhds l)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ℂ
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
have 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
Tactic: lift r to NNReal using h₁.le
Cleared hypotheses: r, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l = if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)
have rw : iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
  (if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)) / (↑n ! : ℂ)
Tactic: rw [← div_mul_cancel₀ (a := iteratedDeriv _ _ _) (b := ↑n !) (by simp),
    ← eq_div_iff_mul_eq (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
    (if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)) / (↑n ! : ℂ)
have trans : iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
  if n = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * L.sumInvPow l (n + 2)
Tactic: trans if n = 0 then ℘[L - l] l else (n + 1) * L.sumInvPow l (n + 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
⊢ iteratedDeriv n ℘[L - l] l / (↑n ! : ℂ) =
    (if n = 0 then ℘[L - l] l else (↑(n + 1)! : ℂ) * L.sumInvPow l (n + 2)) / (↑n ! : ℂ)
have 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 ! : ℂ)
Tactic: trans if n = 0 then ℘[L - l] l else (n + 1) * L.sumInvPow l (n + 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ (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 ! : ℂ)
have 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! : ℂ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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! : ℂ)
⊢ (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 ! : ℂ)
have 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)! : ℂ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ℂ
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)! : ℂ)
have succ : (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * L.sumInvPow l (n + 1 + 2) =
  (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)) * L.sumInvPow l (n + 1 + 2) /
    (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ))
Tactic: simp [Nat.factorial_succ]
-- 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.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
have refine_1 : HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
Tactic: refine .congr ?_
    ((L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept l₀).mono (.trans ?_ hr))
-- 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₀})ᶜ
refine_1 : HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
⊢ HasFPowerSeriesOnBall ℘'[L - l₀] (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
have refine_2 : Metric.eball x (↑r : ENNReal) ⊆ Metric.closedBall x (↑r : ℝ)
Tactic: refine .congr ?_
    ((L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept l₀).mono (.trans ?_ hr))
-- 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₀})ᶜ
⊢ HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
have this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
Tactic: have := (L.hasFPowerSeriesOnBall_weierstrassPExcept l₀ x r hr0 hr).fderiv
-- 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₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
⊢ HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
have h : L.derivWeierstrassPExceptSeries l₀ x =
  ContinuousLinearMap.compFormalMultilinearSeries ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
    (L.weierstrassPExceptSeries l₀ x).derivSeries
Tactic: convert! (ContinuousLinearMap.apply ℂ ℂ (1 : ℂ)).comp_hasFPowerSeriesOnBall this
-- 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₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
⊢ L.derivWeierstrassPExceptSeries l₀ x =
    ContinuousLinearMap.compFormalMultilinearSeries ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
      (L.weierstrassPExceptSeries l₀ x).derivSeries
have h : ∀ (n : ℕ),
  Eq (α := ℂ) ((L.derivWeierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ 1 : ℂ)
    ((ContinuousLinearMap.compFormalMultilinearSeries
            ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
            (L.weierstrassPExceptSeries l₀ x).derivSeries n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
Tactic: ext n
-- 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₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
n : ℕ
⊢ Eq (α := ℂ) ((L.derivWeierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ 1 : ℂ)
    ((ContinuousLinearMap.compFormalMultilinearSeries
            ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
            (L.weierstrassPExceptSeries l₀ x).derivSeries n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
have h : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 *
    (L.sumInvPow x (n + 3) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 3))⁻¹ else 0) =
  HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 *
    ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) *
      (L.sumInvPow x (n + 1 + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 1 + 2))⁻¹ else 0))
Tactic: simp [weierstrassPExceptSeries, derivWeierstrassPExceptSeries]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ℂ
⊢ HasFPowerSeriesAt (𝕜 := ℂ) ℘'[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * L.sumInvPow l (i + 3))
    l
have obtain : ∀ (r : ℝ) (h₁ : 0 < r) (h₂ : Metric.closedBall l r ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ),
  HasFPowerSeriesAt (𝕜 := ℂ) ℘'[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * L.sumInvPow l (i + 3))
    l
Tactic: obtain ⟨r, h₁, h₂⟩ := Metric.nhds_basis_closedBall.mem_iff.mp
    (L.compl_lattice_diff_singleton_mem_nhds l)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘'[L - l] l = (↑(n + 2)! : ℂ) * L.sumInvPow l (n + 3)
have this : iteratedDeriv n ℘'[L - l] l / (↑n ! : ℂ) =
  HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3)
Tactic: have : iteratedDeriv n ℘'[L - l] l / n ! = (↑n + 1) * (↑n + 2) * L.sumInvPow l (n + 3) := by
    simpa using congr($((L.analyticAt_derivWeierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_derivWeierstrassPExcept l)).coeff n)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ℂ
n : ℕ
this :
  iteratedDeriv n ℘'[L - l] l / (↑n ! : ℂ) =
    HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3)
⊢ iteratedDeriv n ℘'[L - l] l = (↑(n + 2)! : ℂ) * L.sumInvPow l (n + 3)
have simp : ∀
  (this :
    iteratedDeriv n ℘'[L - l] l =
      HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3) * (↑n ! : ℂ)),
  iteratedDeriv n ℘'[L - l] l =
    (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)) * L.sumInvPow l (n + 3)
Tactic: simp [div_eq_iff, Nat.factorial_ne_zero, Nat.factorial_succ] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
⊢ Eq (α := (x : ℂ) → FormalMultilinearSeries ℂ ℂ ℂ)
    (fun (x : ℂ) ↦
      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))
    fun (x : ℂ) ↦
    FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      if i = 0 then ℘[L] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow x (i + 2)
have h : ∀ (z : ℂ) (i : ℕ) (f : i = 0), ℘[L - l₀] = ℘[L]
Tactic: congr! with z i f
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
h : ∀ (z : ℂ) (i : ℕ) (f : i = 0), ℘[L - l₀] = ℘[L]
⊢ Eq (α := (x : ℂ) → FormalMultilinearSeries ℂ ℂ ℂ)
    (fun (x : ℂ) ↦
      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))
    fun (x : ℂ) ↦
    FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      if i = 0 then ℘[L] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow x (i + 2)
have h₁ : ∀ (z : ℂ) (i : ℕ),
  ¬i = 0 → (L.sumInvPow z (i + 2) - if l₀ ∈ L.lattice then ((l₀ - z) ^ (i + 2))⁻¹ else 0) = L.sumInvPow z (i + 2)
Tactic: congr! with z i f
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
z : ℂ
i : ℕ
f : i = 0
⊢ ℘[L - l₀] = ℘[L]
have h : ℘[L] = ℘[L]
Tactic: rw [L.weierstrassPExcept_of_notMem _ hl₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
i : ℕ
⊢ (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
have simp_rw : (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
Tactic: simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    L.coeff_weierstrassPExceptSeries,
    ← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
i : ℕ
simp_rw : (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
⊢ (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
have simp_rw₁ : Eq (α := ℂ) (∑' (l : ↥L.lattice), L.weierstrassPExceptSummand (L.ω₁ / 2) x i l)
  (∑' (l : ↥L.lattice), L.weierstrassPSummand x i l)
Tactic: simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    L.coeff_weierstrassPExceptSeries,
    ← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPSummand x b c * (z - x) ^ b)
have simp_rw : Summable (α := ℂ) (β := ℕ × ↥L.lattice)
  (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand (L.ω₁ / 2) x b c * (z - x) ^ b)
Tactic: simp_rw [← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ HasSum (fun (i : ℕ) ↦ (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (℘[L] z)
have simp_rw : HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L - L.ω₁ / 2] z)
Tactic: simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ (↑L.lattice : Set ℂ)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPSeries x) x (↑r : ENNReal)
have simp_rw : HasFPowerSeriesOnBall ℘[L - L.ω₁ / 2] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x (↑r : ENNReal)
Tactic: simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
⊢ MeromorphicAt ℘[L] x
have pos : ∀ (hx : x ∈ L.lattice), MeromorphicAt ℘[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), MeromorphicAt ℘[L] x
⊢ MeromorphicAt ℘[L] x
have neg : ∀ (hx : x ∉ L.lattice), MeromorphicAt ℘[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
⊢ MeromorphicAt ℘[L] x
have pos : MeromorphicAt (E := ℂ)
  (fun (x_1 : ℂ) ↦ ℘[L - x] x_1 + (1 / HPow.hPow (β := ℕ) (x_1 - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
Tactic: simp_rw [← funext <| L.weierstrassPExcept_add ⟨x, hx⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ MeromorphicAt (E := ℂ)
    (fun (x_1 : ℂ) ↦ ℘[L - x] x_1 + (1 / HPow.hPow (β := ℕ) (x_1 - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
have this : MeromorphicAt ℘[L - x] x
Tactic: have := (analyticOnNhd_weierstrassPExcept L x x (by simp)).meromorphicAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ Meromorphic ℘'[L]
have rw : Meromorphic (deriv ℘[L])
Tactic: rw [← deriv_weierstrassP]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = -2
have trans : meromorphicOrderAt ℘[L] l₀ = (↑(-2) : WithTop ℤ)
Tactic: trans ↑(-2 : ℤ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
trans : meromorphicOrderAt ℘[L] l₀ = (↑(-2) : WithTop ℤ)
⊢ meromorphicOrderAt ℘[L] l₀ = -2
have trans₁ : Eq (α := WithTop ℤ) (↑(-2) : WithTop ℤ) (-2)
Tactic: trans ↑(-2 : ℤ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = (↑(-2) : WithTop ℤ)
have rw : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = HPow.hPow (β := ℤ) (z - l₀) (-2) • g z
Tactic: rw [meromorphicOrderAt_eq_int_iff (L.meromorphic_weierstrassP l₀)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = HPow.hPow (β := ℤ) (z - l₀) (-2) • g z
have refine_1 : AnalyticAt ℂ (F := ℂ)
  (fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
  l₀
Tactic: refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
refine_1 :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀
⊢ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = HPow.hPow (β := ℤ) (z - l₀) (-2) • g z
have refine_2 : Ne (α := ℂ)
  ((fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀)
  0
Tactic: refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
refine_1 :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀
refine_2 :
  Ne (α := ℂ)
    ((fun (z : ℂ) ↦
        HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
      l₀)
    0
⊢ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = HPow.hPow (β := ℤ) (z - l₀) (-2) • g z
have refine_3 : ∀ᶠ (z : ℂ) in 𝓝[≠] l₀,
  ℘[L] z =
    HSMul.hSMul (β := ℂ) (HPow.hPow (β := ℤ) (z - l₀) (-2))
      ((fun (z : ℂ) ↦
          HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
        z)
Tactic: refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀
have this : AnalyticAt ℂ ℘[L - l₀] l₀
Tactic: have : AnalyticAt ℂ ℘[L - l₀] l₀ := L.analyticOnNhd_weierstrassPExcept l₀ l₀ (by simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀
have refine_1 : AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀
Tactic: suffices AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀ by fun_prop