awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this_1 : AnalyticAt ℂ ℘[L - l₀] l₀
this : AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
refine_1 : AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀

Tactic:
suffices AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀ by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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₀
neg :
  ∀ (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₀

Tactic:
by_cases hl₀ : l₀ = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
hl₀ : l₀ = 0
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀

Tactic:
simpa [hl₀] using analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
hl₀ : ¬l₀ = 0
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2) l₀

Tactic:
fun_prop (disch := simpa)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ Ne (α := ℂ)
    ((fun (z : ℂ) ↦
        HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
      l₀)
    0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
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)
⊢ 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)

Tactic:
(hz : _ ≠ _)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
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)
⊢ ∀ᶠ (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:
filter_upwards [self_mem_nhdsWithin] with z (hz : _ ≠ _)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
hz : z ≠ l₀
⊢ HPow.hPow (β := ℕ) (z - l₀) 2 ≠ 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
hz : z ≠ l₀
⊢ HPow.hPow (β := ℕ) (z - l₀) 2 ≠ 0

Tactic:
have : (z - l₀) ^ 2 ≠ 0 := by simpa [sub_eq_zero]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
hz : z ≠ l₀
this : HPow.hPow (β := ℕ) (z - l₀) 2 ≠ 0
⊢ ℘[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:
simp [← L.ite_eq_one_sub_sq_mul_weierstrassP l₀ h,
        if_neg hz, inv_mul_cancel_left₀ this, zpow_ofNat]

Premises used: PeriodPair.ite_eq_one_sub_sq_mul_weierstrassP, inv_mul_cancel_left₀, zpow_ofNat, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ Eq (α := WithTop ℤ) (↑(-2) : WithTop ℤ) (-2)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
h : ∀ (x : ℕ), L.sumInvPow 0 x = L.G x
⊢ L.sumInvPow 0 = L.G

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℕ
⊢ L.sumInvPow 0 x = L.G x

Tactic:
simp [sumInvPow, G]

Premises used: PeriodPair.G, PeriodPair.sumInvPow
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
n : ℕ
hn : Odd n
rw :
  Eq (α := ℂ)
    (∑' (c : ↥L.lattice), (HPow.hPow (α := ℂ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) n)⁻¹)
    (∑' (b : ↥L.lattice), -((↑b : ℂ) ^ n)⁻¹)
⊢ L.G n = 0

Tactic:
rw [← CharZero.eq_neg_self_iff, G, ← tsum_neg, ← (Equiv.neg _).tsum_eq]

Premises used: Equiv.neg, Equiv.tsum_eq, PeriodPair.G, CharZero.eq_neg_self_iff, tsum_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
n : ℕ
hn : Odd n
e_f :
  ∀ (l : ↥L.lattice),
    (HPow.hPow (α := ℂ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) n)⁻¹ = -((↑l : ℂ) ^ n)⁻¹
⊢ Eq (α := ℂ)
    (∑' (c : ↥L.lattice), (HPow.hPow (α := ℂ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) n)⁻¹)
    (∑' (b : ↥L.lattice), -((↑b : ℂ) ^ n)⁻¹)

Tactic:
congr with l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
n : ℕ
hn : Odd n
l : ↥L.lattice
⊢ (HPow.hPow (α := ℂ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) n)⁻¹ = -((↑l : ℂ) ^ n)⁻¹

Tactic:
simp only [Equiv.neg_apply, NegMemClass.coe_neg, neg_inv, hn.neg_pow]

Premises used: Odd.neg_pow, Equiv.neg_apply, neg_inv, NegMemClass.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Meromorphic (E := ℂ) fun (z : ℂ) ↦
    HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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

Tactic:
fun z ↦ (this _).congr ?_

Premises used: Meromorphic, MeromorphicAt.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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₃
refine :
  ∀ (z : ℂ),
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝[≠] z]
      L.relation
⊢ Meromorphic L.relation

Tactic:
refine fun z ↦ (this _).congr ?_

Premises used: MeromorphicAt.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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 : ℂ
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
⊢ (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝[≠] z]
    L.relation

Tactic:
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds
    (L.compl_lattice_diff_singleton_mem_nhds _)] with w hw hw'

Premises used: PeriodPair.compl_lattice_diff_singleton_mem_nhds, mem_nhdsWithin_of_mem_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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})ᶜ
⊢ w ∉ L.lattice

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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₃
h₁ 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₃
⊢ HPow.hPow (β := ℕ) (℘'[L] w) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] w) 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w

Tactic:
rw [relation, if_neg (by simp_all)]

Premises used: _private.0.PeriodPair.relation, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
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
⊢ 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

Tactic:
filter_upwards [L.compl_lattice_diff_singleton_mem_nhds _] with z hz

Premises used: PeriodPair.compl_lattice_diff_singleton_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
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
⊢ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
hz0 : z = 0
pos : 0 = HPow.hPow (α := ℂ) (β := ℕ) 2 2 - 4
⊢ (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:
simp [hz0, relation]

Premises used: _private.0.PeriodPair.relation
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
hz0 : z = 0
⊢ 0 = HPow.hPow (α := ℂ) (β := ℕ) 2 2 - 4

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
hz0 : ¬z = 0
⊢ z ∉ L.lattice

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hz : z ∈ ((↑L.lattice : Set ℂ) \ {0})ᶜ
hz0 : ¬z = 0
⊢ z ∉ L.lattice

Tactic:
replace hz : z ∉ L.lattice := by simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hz0 : ¬z = 0
hz : z ∉ L.lattice
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
⊢ (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:
simp only [Pi.mul_apply, Pi.pow_apply, relation, ↓reduceIte, hz,
    ← ZeroMemClass.coe_zero L.lattice, L.derivWeierstrassPExcept_def, L.weierstrassPExcept_def]

Premises used: Pi.mul_apply, PeriodPair.weierstrassPExcept_def, Pi.pow_apply, ZeroMemClass.coe_zero, _private.0.PeriodPair.relation, reduceIte, PeriodPair.lattice, PeriodPair.derivWeierstrassPExcept_def
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hz0 : ¬z = 0
hz : z ∉ L.lattice
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
⊢ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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 (β := ℕ) 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:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ AnalyticAt ℂ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0

Tactic:
.congr ?_ L.relation_mul_id_pow_six_eventuallyEq.symm

Premises used: _private.0.PeriodPair.relation_mul_id_pow_six_eventuallyEq, AnalyticAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
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
⊢ AnalyticAt ℂ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0

Tactic:
refine .congr ?_ L.relation_mul_id_pow_six_eventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ 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:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
⊢ L.relation (-x) = L.relation x

Tactic:
simp [relation]

Premises used: _private.0.PeriodPair.relation
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
⊢ L.relation (-x) = L.relation x

Tactic:
classical simp [relation]

Premises used: _private.0.PeriodPair.relation
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
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
⊢ iteratedDeriv 6 (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]

Premises used: _private.0.PeriodPair.relation_mul_id_pow_six_eventuallyEq, Filter.EventuallyEq.iteratedDeriv_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
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
⊢ 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:
simp_rw [pow_succ (_ + _), pow_succ (_ - _), pow_zero, one_mul]

Premises used: pow_succ, HSub.hSub, pow_zero, HAdd.hAdd, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Odd (α := ℕ) 3

Tactic:
decide
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Nat.choose 6 4 = 15

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Nat.choose 6 3 = 20

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ -(2 * (20 * ((↑5! : ℂ) * L.G 6) * (↑3! : ℂ))) + -(20 * ((↑5! : ℂ) * L.G 6) * (↑3! : ℂ) * 2) -
        4 * (15 * ((↑5! : ℂ) * L.G 6) * 2 + (15 * ((↑5! : ℂ) * L.G 6) * 2 + 15 * ((↑5! : ℂ) * L.G 6) * 2)) +
      140 * L.G 6 * (↑6! : ℂ) =
    0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ L.relation 0 = 0

Tactic:
simp [relation]

Premises used: _private.0.PeriodPair.relation
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
refine : 1 ≤ meromorphicOrderAt L.relation 0
⊢ AnalyticAt ℂ L.relation 0

Tactic:
refine .of_meromorphicOrderAt_pos (one_pos.trans_le ?_) (by simp [relation])
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
⊢ MeromorphicAt L.relation 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
⊢ MeromorphicAt (HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + meromorphicOrderAt (HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
⊢ MeromorphicAt (𝕜 := ℂ) id 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
⊢ 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

Premises used: meromorphicOrderAt_mul, meromorphicOrderAt_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + (↑6 : WithTop ℤ) * meromorphicOrderAt (𝕜 := ℂ) id 0
⊢ Ne (α := WithTop ℤ) 6 ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + (↑6 : WithTop ℤ) * meromorphicOrderAt (𝕜 := ℂ) id 0
rw : HAdd.hAdd (α := WithTop ℤ) 1 6 ≤ meromorphicOrderAt L.relation 0 + 6
⊢ 1 ≤ meromorphicOrderAt L.relation 0

Tactic:
rw [← WithTop.add_le_add_iff_right (z := 6) (by simp)]

Premises used: WithTop.add_le_add_iff_right
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + (↑6 : WithTop ℤ) * meromorphicOrderAt (𝕜 := ℂ) id 0
⊢ HAdd.hAdd (α := WithTop ℤ) 1 6 ≤ meromorphicOrderAt L.relation 0 + 6

Tactic:
simpa [-add_le_add_iff_left_of_ne_top] using this

Premises used: add_le_add_iff_left_of_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
suffices : 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0
⊢ 1 ≤ meromorphicOrderAt L.relation 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
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ AnalyticAt ℂ (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0

Tactic:
fun_prop