awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ) = 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)
have e_f : ∀ (l : ↥L.lattice),
  HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - if (↑l : ℂ) = l₀ then (HPow.hPow (β := ℤ) (l₀ - x) (↑(i + 3) : ℤ))⁻¹ else 0) =
    if (↑l : ℂ) = l₀ then 0
    else HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑(i + 1 + 2) : ℤ))⁻¹ - 0 i
Tactic: congr with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - if (↑l : ℂ) = l₀ then (HPow.hPow (β := ℤ) (l₀ - x) (↑(i + 3) : ℤ))⁻¹ else 0) =
    if (↑l : ℂ) = l₀ then 0
    else HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑(i + 1 + 2) : ℤ))⁻¹ - 0 i
have pos : ∀ (e : (↑l : ℂ) = l₀),
  HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - (HPow.hPow (β := ℤ) (l₀ - x) (↑(i + 3) : ℤ))⁻¹) = 0
Tactic: split_ifs with e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
pos :
  ∀ (e : (↑l : ℂ) = l₀),
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - (HPow.hPow (β := ℤ) (l₀ - x) (↑(i + 3) : ℤ))⁻¹) = 0
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - if (↑l : ℂ) = l₀ then (HPow.hPow (β := ℤ) (l₀ - x) (↑(i + 3) : ℤ))⁻¹ else 0) =
    if (↑l : ℂ) = l₀ then 0
    else HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑(i + 1 + 2) : ℤ))⁻¹ - 0 i
have neg : ∀ (e : ¬(↑l : ℂ) = l₀),
  HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - 0) =
    HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑(i + 1 + 2) : ℤ))⁻¹ - 0 i
Tactic: split_ifs with e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬(↑l : ℂ) = l₀
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - 0) =
    HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (((↑l : ℂ) - x) ^ (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 + 2))⁻¹ - 0
have neg : (↑(i + 2) : ℂ) * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1 + 1) : ℂ) * (((↑l : ℂ) - x) ^ (i + 1 + 2))⁻¹ - 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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) - 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 h₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀
Tactic: have h₁ (l : L.lattice) : l.1 ≠ l₀ := fun e ↦ hl₀ (e ▸ l.2)
-- 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 =
    ∑' (l : ↥L.lattice),
      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 : ℂ)
have zero : 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))
    0 =
  ∑' (l : ↥L.lattice),
    if (↑l : ℂ) = l₀ then 0
    else
      HSub.hSub (β := ℂ)
        (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(HAdd.hAdd (α := ℕ) 0 2) : ℤ)))
        (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) 0 (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
Tactic: cases i with
  | zero => simp [weierstrassPExcept, sub_sq_comm x, zpow_ofNat]
  | succ i =>
    split_ifs with hl₀
    · trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)
      · rw [FormalMultilinearSeries.coeff_ofScalars, tsum_ite_eq, zpow_neg, zpow_natCast]
        simp [add_assoc, one_add_one_eq_two]
      · rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
        · simp_rw [Subtype.ext_iff, zpow_neg]
          congr with l
          split_ifs with e
          · simp only [e, zpow_natCast, sub_self, mul_zero]
          · dsimp; norm_cast; ring
        · exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))
    · have h₁ (l : L.lattice) : l.1 ≠ l₀ := fun e ↦ hl₀ (e ▸ l.2)
      simp [h₁, tsum_mul_left, sumInvPow, add_assoc,
        one_add_one_eq_two, ← zpow_natCast, -neg_add_rev]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
zero :
  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))
      0 =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(HAdd.hAdd (α := ℕ) 0 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) 0 (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 =
    ∑' (l : ↥L.lattice),
      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 : ℂ)
have succ : ∀ (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 : ℂ)
Tactic: cases i with
  | zero => simp [weierstrassPExcept, sub_sq_comm x, zpow_ofNat]
  | succ i =>
    split_ifs with hl₀
    · trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)
      · rw [FormalMultilinearSeries.coeff_ofScalars, tsum_ite_eq, zpow_neg, zpow_natCast]
        simp [add_assoc, one_add_one_eq_two]
      · rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
        · simp_rw [Subtype.ext_iff, zpow_neg]
          congr with l
          split_ifs with e
          · simp only [e, zpow_natCast, sub_self, mul_zero]
          · dsimp; norm_cast; ring
        · exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))
    · have h₁ (l : L.lattice) : l.1 ≠ l₀ := fun e ↦ hl₀ (e ▸ l.2)
      simp [h₁, tsum_mul_left, sumInvPow, add_assoc,
        one_add_one_eq_two, ← zpow_natCast, -neg_add_rev]
Cleared hypotheses: 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‖
⊢ ∃ (κ : ℝ), 1 < κ ∧ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
have obtain : ∀ (κ : ℝ) (hκ : κ > 0)
  (hκ' :
    Subset (α := Set ℝ) (Metric.ball 1 κ)
      ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)),
  ∃ (κ : ℝ), 1 < κ ∧ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
Tactic: obtain ⟨κ, hκ, hκ'⟩ := Metric.isOpen_iff.mp ((continuous_mul_const ‖z - x‖).isOpen_preimage _
      (isClosedMap_dist x _
      (L.isClosed_of_subset_lattice (Set.diff_subset (t := {l₀})))).upperClosure.isOpen_compl) 1
      (by simpa [Complex.dist_eq, @forall_comm ℝ, norm_sub_rev x] using hx)
-- 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‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
⊢ ∃ (κ : ℝ), 1 < κ ∧ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
have refine : ∀ (l : ↥L.lattice) (hl : (↑l : ℂ) ≠ l₀), ‖z - x‖ * (κ / 2 + 1) < ‖(↑l : ℂ) - x‖
Tactic: refine ⟨κ / 2 + 1, by simpa, fun l hl ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
l : ↥L.lattice
hl : (↑l : ℂ) ≠ l₀
⊢ ‖z - x‖ * (κ / 2 + 1) < ‖(↑l : ℂ) - x‖
have this : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l
Tactic: have : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l := by
      simpa using @hκ' (κ / 2 + 1) (by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, 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‖
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
have obtain : ∀ (κ : ℝ) (hκ : 1 < κ) (hκ' : ∀ (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: obtain ⟨κ, hκ, hκ'⟩ : ∃ κ : ℝ, 1 < κ ∧ ∀ l : L.lattice, l.1 ≠ l₀ → ‖z - x‖ * κ < ‖l - x‖ := by
    obtain ⟨κ, hκ, hκ'⟩ := Metric.isOpen_iff.mp ((continuous_mul_const ‖z - x‖).isOpen_preimage _
      (isClosedMap_dist x _
      (L.isClosed_of_subset_lattice (Set.diff_subset (t := {l₀})))).upperClosure.isOpen_compl) 1
      (by simpa [Complex.dist_eq, @forall_comm ℝ, norm_sub_rev x] using hx)
    refine ⟨κ / 2 + 1, by simpa, fun l hl ↦ ?_⟩
    have : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l := by
      simpa using @hκ' (κ / 2 + 1) (by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ])
    simpa only [Complex.dist_eq, norm_sub_rev x, mul_comm] using this _ l.2 hl
-- 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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
have rw : Summable (α := ℂ) (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
  (Function.comp (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
    (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
Tactic: rw [← e.symm.summable_iff]
-- 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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ Summable (α := ℂ) (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
    (Function.comp (β := ℕ × ↥L.lattice)
      (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
      (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
have h₁ : Summable (α := ℂ) (β := ↥L.lattice)
  (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
    (Function.comp (β := ℕ × ↥L.lattice)
      (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
      (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
    Sum.inl)
Tactic: apply Summable.sum
-- 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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
h₁ :
  Summable (α := ℂ) (β := ↥L.lattice)
    (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
      (Function.comp (β := ℕ × ↥L.lattice)
        (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
        (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
      Sum.inl)
⊢ Summable (α := ℂ) (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
    (Function.comp (β := ℕ × ↥L.lattice)
      (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
      (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
have h₂ : Summable (α := ℂ) (β := ℕ × ↥L.lattice)
  (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
    (Function.comp (β := ℕ × ↥L.lattice)
      (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
      (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
    Sum.inr)
Tactic: apply Summable.sum
-- 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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
      (Function.comp (β := ℕ × ↥L.lattice)
        (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
        (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
      Sum.inr)
have h₂ : Summable (α := ℂ) fun (x_1 : ℕ × ↥L.lattice) ↦
  (if (↑x_1.2 : ℂ) = l₀ then 0
    else
      HAdd.hAdd (α := ℂ) (↑(x_1.1 + 1) : ℂ) 1 * ((↑x_1.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑x_1.1 : ℤ) 1 + 2)) - 0) *
    (z - x) ^ (x_1.1 + 1)
Tactic: dsimp [e, Function.comp_def, Function.uncurry_def, Denumerable.eqv, weierstrassPExceptSummand]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
have this : |κ⁻¹| < 1
Tactic: have : |κ⁻¹| < 1 := by grind [abs_inv, inv_lt_one_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ Summable (α := ℂ) fun (x_1 : ℕ × ↥L.lattice) ↦
    (if (↑x_1.2 : ℂ) = l₀ then 0
      else
        HAdd.hAdd (α := ℂ) (↑(x_1.1 + 1) : ℂ) 1 * ((↑x_1.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑x_1.1 : ℤ) 1 + 2)) - 0) *
      (z - x) ^ (x_1.1 + 1)
have H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
Tactic: have H₁ : Summable fun i : ℕ ↦ ((i + 2) * κ ^ (-i : ℤ)) := by
      have : |κ⁻¹| < 1 := by grind [abs_inv, inv_lt_one_iff₀]
      simpa [mul_comm] using ((Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero 1 2).hasSum
        (y := κ⁻¹) (by simpa [enorm_eq_nnnorm])).summable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
⊢ Summable (α := ℂ) fun (x_1 : ℕ × ↥L.lattice) ↦
    (if (↑x_1.2 : ℂ) = l₀ then 0
      else
        HAdd.hAdd (α := ℂ) (↑(x_1.1 + 1) : ℂ) 1 * ((↑x_1.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑x_1.1 : ℤ) 1 + 2)) - 0) *
      (z - x) ^ (x_1.1 + 1)
have H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
Tactic: have H₂ : Summable fun l : L.lattice ↦ ‖l - x‖ ^ (-3 : ℤ) * ‖z - x‖ :=
      (ZLattice.summable_norm_sub_zpow _ _ (by simp) _).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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
⊢ Summable (α := ℂ) fun (x_1 : ℕ × ↥L.lattice) ↦
    (if (↑x_1.2 : ℂ) = l₀ then 0
      else
        HAdd.hAdd (α := ℂ) (↑(x_1.1 + 1) : ℂ) 1 * ((↑x_1.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑x_1.1 : ℤ) 1 + 2)) - 0) *
      (z - x) ^ (x_1.1 + 1)
have h₂ : ∀ (i : ℕ × ↥L.lattice),
  ‖(if (↑i.2 : ℂ) = l₀ then 0
        else HAdd.hAdd (α := ℂ) (↑(i.1 + 1) : ℂ) 1 * ((↑i.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑i.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (i.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑i.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑i.2 : ℂ) - x‖ (-3) * ‖z - x‖)
Tactic: refine (H₁.mul_of_nonneg H₂ (by intro; positivity) (by intro; positivity)).of_norm_bounded ?_
-- 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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
⊢ ‖(if (↑p.2 : ℂ) = l₀ then 0
        else HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
have pos : ∀ (hp : (↑p.2 : ℂ) = l₀),
  ‖0 * (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
Tactic: split_ifs with hp
-- 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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
pos :
  ∀ (hp : (↑p.2 : ℂ) = l₀),
    ‖0 * (z - x) ^ (p.1 + 1)‖ ≤
      HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
        (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
⊢ ‖(if (↑p.2 : ℂ) = l₀ then 0
        else HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
have neg : ∀ (hp : ¬(↑p.2 : ℂ) = l₀),
  ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
Tactic: split_ifs with hp
-- 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‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : (↑p.2 : ℂ) = l₀
⊢ ‖0 * (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
have pos : 0 ≤ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * (κ ^ p.1)⁻¹ * ((HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)
Tactic: simp only [zero_mul, norm_zero, zpow_neg, zpow_natCast, Int.reduceNeg]