awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 / HPow.hPow (β := ℕ) l₀ 2) l₀
have pos : ∀ (hl₀ : l₀ = 0), AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀
Tactic: by_cases hl₀ : l₀ = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
pos : ∀ (hl₀ : l₀ = 0), AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀
have neg : ∀ (hl₀ : ¬l₀ = 0), AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀
Tactic: by_cases hl₀ : l₀ = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
⊢ Membership.mem (γ := Set ℂ) {l₀}ᶜ z →
    ℘[L] z =
      HPow.hPow (β := ℤ) (z - l₀) (-2) •
        (HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
have h₁ : ∀ (hz : z ≠ l₀),
  ℘[L] z =
    HPow.hPow (β := ℤ) (z - l₀) (-2) •
      (HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
Tactic: (hz : _ ≠ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∀ᶠ (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)
have h₁ : ∀ (z : ℂ) (hz : z ≠ l₀),
  ℘[L] z =
    HPow.hPow (β := ℤ) (z - l₀) (-2) •
      (HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
Tactic: filter_upwards [self_mem_nhdsWithin] with z (hz : _ ≠ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
hz : z ≠ l₀
⊢ ℘[L] z =
    HPow.hPow (β := ℤ) (z - l₀) (-2) •
      (HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
have this : HPow.hPow (β := ℕ) (z - l₀) 2 ≠ 0
Tactic: have : (z - l₀) ^ 2 ≠ 0 := by simpa [sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ L.sumInvPow 0 = L.G
have h : ∀ (x : ℕ), L.sumInvPow 0 x = L.G x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
n : ℕ
hn : Odd n
⊢ L.G n = 0
have rw : Eq (α := ℂ)
  (∑' (c : ↥L.lattice), (HPow.hPow (α := ℂ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) n)⁻¹)
  (∑' (b : ↥L.lattice), -((↑b : ℂ) ^ n)⁻¹)
Tactic: rw [← CharZero.eq_neg_self_iff, G, ← tsum_neg, ← (Equiv.neg _).tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
n : ℕ
hn : Odd n
⊢ Eq (α := ℂ)
    (∑' (c : ↥L.lattice), (HPow.hPow (α := ℂ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) n)⁻¹)
    (∑' (b : ↥L.lattice), -((↑b : ℂ) ^ n)⁻¹)
have e_f : ∀ (l : ↥L.lattice),
  (HPow.hPow (α := ℂ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) n)⁻¹ = -((↑l : ℂ) ^ n)⁻¹
Tactic: congr with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
⊢ Meromorphic L.relation
have this : Meromorphic (E := ℂ) fun (z : ℂ) ↦
  HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃
Tactic: have : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃ := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
this :
  Meromorphic (E := ℂ) fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃
⊢ Meromorphic L.relation
have refine : ∀ (z : ℂ),
  (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝[≠] z]
    L.relation
Tactic: refine fun z ↦ (this _).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
this :
  Meromorphic (E := ℂ) fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃
z : ℂ
⊢ (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝[≠] z]
    L.relation
have h : ∀ (w : ℂ) (hw : Membership.mem (γ := Set ℂ) {z}ᶜ w) (hw' : w ∈ ((↑L.lattice : Set ℂ) \ {z})ᶜ),
  HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w
Tactic: filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds
    (L.compl_lattice_diff_singleton_mem_nhds _)] with w hw hw'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
this :
  Meromorphic (E := ℂ) fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : Membership.mem (γ := Set ℂ) {z}ᶜ w
hw' : w ∈ ((↑L.lattice : Set ℂ) \ {z})ᶜ
⊢ HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w
have h : HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃ =
  if w ∈ L.lattice then 0 else HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃
Tactic: rw [relation, if_neg (by simp_all)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
this :
  Meromorphic (E := ℂ) fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : Membership.mem (γ := Set ℂ) {z}ᶜ w
hw' : w ∈ ((↑L.lattice : Set ℂ) \ {z})ᶜ
h :
  HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃ =
    if w ∈ L.lattice then 0
    else HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃
⊢ HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w
have h₁ : HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃ =
  HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃
Tactic: rw [relation, if_neg (by simp_all)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6 =ᶠ[𝓝 0] fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
have h : ∀ (z : ℂ) (hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ),
  (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
Tactic: filter_upwards [L.compl_lattice_diff_singleton_mem_nhds _] with z hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
⊢ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
have pos : ∀ (hz0 : z = 0),
  (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
Tactic: by_cases hz0 : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
pos :
  ∀ (hz0 : z = 0),
    (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
      HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
            4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
          L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
        L.g₃ * HPow.hPow (β := ℕ) z 6
⊢ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
have neg : ∀ (hz0 : ¬z = 0),
  (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
Tactic: by_cases hz0 : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
hz0 : z = 0
⊢ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
have pos : 0 = HPow.hPow (α := ℂ) (β := ℕ) 2 2 - 4
Tactic: simp [hz0, relation]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
hz0 : ¬z = 0
⊢ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
have hz₁ : z ∉ L.lattice
Tactic: replace hz : z ∉ L.lattice := by simp_all
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
hz0 : ¬z = 0
hz : z ∉ L.lattice
⊢ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) z =
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
have neg : (HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) *
    HPow.hPow (β := ℕ) (id z) 6 =
  HPow.hPow (β := ℕ) ((℘'[L] z + 2 / HPow.hPow (β := ℕ) (z - (↑0 : ℂ)) 3) * HPow.hPow (β := ℕ) z 3 - 2) 2 -
        4 *
          HPow.hPow (β := ℕ)
            ((℘[L] z + (1 / HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑0 : ℂ)) 2)) *
                HPow.hPow (β := ℕ) z 2 +
              1)
            3 +
      L.g₂ *
        ((℘[L] z + (1 / HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑0 : ℂ)) 2)) *
            HPow.hPow (β := ℕ) z 6 +
          HPow.hPow (β := ℕ) z 4) +
    L.g₃ * HPow.hPow (β := ℕ) z 6
Tactic: simp only [Pi.mul_apply, Pi.pow_apply, relation, ↓reduceIte, hz,
    ← ZeroMemClass.coe_zero L.lattice, L.derivWeierstrassPExcept_def, L.weierstrassPExcept_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
hz0 : ¬z = 0
hz : z ∉ L.lattice
⊢ (HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) *
      HPow.hPow (β := ℕ) (id z) 6 =
    HPow.hPow (β := ℕ) ((℘'[L] z + 2 / HPow.hPow (β := ℕ) (z - (↑0 : ℂ)) 3) * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 *
            HPow.hPow (β := ℕ)
              ((℘[L] z + (1 / HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑0 : ℂ)) 2)) *
                  HPow.hPow (β := ℕ) z 2 +
                1)
              3 +
        L.g₂ *
          ((℘[L] z + (1 / HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑0 : ℂ)) 2)) *
              HPow.hPow (β := ℕ) z 6 +
            HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6
have neg : (HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) * HPow.hPow (β := ℕ) z 6 =
  HPow.hPow (β := ℕ) ((℘'[L] z + 2 / HPow.hPow (β := ℕ) z 3) * HPow.hPow (β := ℕ) z 3 - 2) 2 -
        4 * HPow.hPow (β := ℕ) ((℘[L] z + -(HPow.hPow (β := ℕ) z 2)⁻¹) * HPow.hPow (β := ℕ) z 2 + 1) 3 +
      L.g₂ * ((℘[L] z + -(HPow.hPow (β := ℕ) z 2)⁻¹) * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
    L.g₃ * HPow.hPow (β := ℕ) z 6
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ AnalyticAt ℂ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
have refine : AnalyticAt ℂ (F := ℂ)
  (fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
          4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
        L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
      L.g₃ * HPow.hPow (β := ℕ) z 6)
  0
Tactic: refine .congr ?_ L.relation_mul_id_pow_six_eventuallyEq.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ iteratedDeriv 6 (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have rw : Eq (α := ℂ)
  (iteratedDeriv 6
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
            4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
          L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
        L.g₃ * HPow.hPow (β := ℕ) z 6)
    0)
  0
Tactic: rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ Eq (α := ℂ)
    (iteratedDeriv 6
      (fun (z : ℂ) ↦
        HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
              4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
            L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
          L.g₃ * HPow.hPow (β := ℕ) z 6)
      0)
    0
have simp_rw : Eq (α := ℂ)
  (iteratedDeriv 6
    (fun (z : ℂ) ↦
      (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) * (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) -
            4 *
              ((℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) * (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) *
                (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1)) +
          L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
        L.g₃ * HPow.hPow (β := ℕ) z 6)
    0)
  0
Tactic: simp_rw [pow_succ (_ + _), pow_succ (_ - _), pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ AnalyticAt ℂ L.relation 0
have refine : 1 ≤ meromorphicOrderAt L.relation 0
Tactic: refine .of_meromorphicOrderAt_pos (one_pos.trans_le ?_) (by simp [relation])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
⊢ 1 ≤ meromorphicOrderAt L.relation 0
have this₁ : 7 ≤ meromorphicOrderAt L.relation 0 + (↑6 : WithTop ℤ) * meromorphicOrderAt (𝕜 := ℂ) id 0
Tactic: rw [meromorphicOrderAt_mul (by fun_prop) (by fun_prop),
      meromorphicOrderAt_pow (by fun_prop)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + (↑6 : WithTop ℤ) * meromorphicOrderAt (𝕜 := ℂ) id 0
⊢ 1 ≤ meromorphicOrderAt L.relation 0
have rw : HAdd.hAdd (α := WithTop ℤ) 1 6 ≤ meromorphicOrderAt L.relation 0 + 6
Tactic: rw [← WithTop.add_le_add_iff_right (z := 6) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ 1 ≤ meromorphicOrderAt L.relation 0
have suffices : 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
Tactic: suffices 7 ≤ meromorphicOrderAt (L.relation * id ^ 6) 0 by
    rw [meromorphicOrderAt_mul (by fun_prop) (by fun_prop),
      meromorphicOrderAt_pow (by fun_prop)] at this
    rw [← WithTop.add_le_add_iff_right (z := 6) (by simp)]
    simpa [-add_le_add_iff_left_of_ne_top] using this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
have rw : LE.le (α := WithTop ℤ) 7
  (ENat.map Nat.cast (analyticOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0))
Tactic: rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ LE.le (α := WithTop ℤ) 7
    (ENat.map Nat.cast (analyticOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0))
have refine : ∀ (i : ℕ) (hi₁ : i < 7), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
Tactic: refine ENat.monotone_map_iff.mpr Nat.mono_cast
    ((natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (by fun_prop)).mpr fun i hi₁ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have pos : ∀ (hi₂ : Odd i), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
Tactic: by_cases hi₂ : Odd i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
pos : ∀ (hi₂ : Odd i), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have neg : ∀ (hi₂ : ¬Odd i), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
Tactic: by_cases hi₂ : Odd i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have pos : ∀ (hi₃ : i = 0), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
Tactic: by_cases hi₃ : i = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
pos : ∀ (hi₃ : i = 0), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have neg : ∀ (hi₃ : ¬i = 0), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
Tactic: by_cases hi₃ : i = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have pos : ∀ (hi₄ : i = 6), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
Tactic: by_cases hi₄ : i = 6
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
pos : ∀ (hi₄ : i = 6), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have neg : ∀ (hi₄ : ¬i = 6), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
Tactic: by_cases hi₄ : i = 6
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
have neg : Eq (α := ℂ)
  (iteratedDeriv i
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
            4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
          L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
        L.g₃ * HPow.hPow (β := ℕ) z 6)
    0)
  0
Tactic: rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ Eq (α := ℂ)
    (iteratedDeriv i
      (fun (z : ℂ) ↦
        HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
              4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
            L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
          L.g₃ * HPow.hPow (β := ℕ) z 6)
      0)
    0
have neg : Eq (α := ℂ)
  (iteratedDeriv i
    (fun (z : ℂ) ↦
      (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) * (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) -
            4 *
              ((℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) * (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) *
                (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1)) +
          L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
        L.g₃ * HPow.hPow (β := ℕ) z 6)
    0)
  0
Tactic: simp_rw [pow_succ (_ + _), pow_succ (_ - _), pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation (x + (↑l : ℂ)) = L.relation x
have simp : (if x + (↑l : ℂ) ∈ L.lattice then 0
  else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃) =
  if x ∈ L.lattice then 0 else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃
Tactic: simp only [relation, derivWeierstrassP_add_coe, weierstrassP_add_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ (if x + (↑l : ℂ) ∈ L.lattice then 0
    else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃) =
    if x ∈ L.lattice then 0
    else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃
have e_c : (x + (↑l : ℂ) ∈ L.lattice) = (x ∈ L.lattice)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation (x - (↑l : ℂ)) = L.relation x
have rw : L.relation (x - (↑l : ℂ) + (↑l : ℂ)) = L.relation x
Tactic: rw [← L.relation_add_coe _ l, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
rw : L.relation (x - (↑l : ℂ) + (↑l : ℂ)) = L.relation x
⊢ L.relation (x - (↑l : ℂ)) = L.relation x
have rw₁ : L.relation x = L.relation x
Tactic: rw [← L.relation_add_coe _ l, sub_add_cancel]