awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
pos : (↑i : ℂ) = l₀ → DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
neg :
  ¬(↑i : ℂ) = l₀ →
    DifferentiableOn ℂ (F := ℂ)
      (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
      ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : (↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 1) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ ∀ x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ, HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 2 ≠ 0

Tactic:
aesop (add simp sub_eq_zero)

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
exact .sub (.div (by fun_prop) (by fun_prop) (by aesop (add simp sub_eq_zero))) (by fun_prop)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
rw :
  Eq (α := ℂ)
    (∑' (c : ↥L.lattice),
      if (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
      else
        1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 2 -
          1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) 2)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = -l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
⊢ Eq (α := ℂ)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (-z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = -l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)

Tactic:
rw [← (Equiv.neg L.lattice).tsum_eq]

Premises used: Equiv.neg, Equiv.tsum_eq, Membership.mem, Subtype, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
h : ∀ (l : ↥L.lattice), (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀
h₁ :
  ∀ (l : ↥L.lattice),
    ¬(↑l : ℂ) = -l₀ →
      1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ)) 2 -
          1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) 2 =
        1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
⊢ Eq (α := ℂ)
    (∑' (c : ↥L.lattice),
      if (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
      else
        1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 2 -
          1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) 2)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = -l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)

Tactic:
congr! 3 with l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀

Tactic:
simp [neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
h_1 : ¬(↑l : ℂ) = -l₀
h : HPow.hPow (β := ℕ) (-z + (↑l : ℂ)) 2 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2
⊢ 1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ)) 2 -
      1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) 2 =
    1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
h : ¬(↑l : ℂ) = -l₀
⊢ HPow.hPow (β := ℕ) (-z + (↑l : ℂ)) 2 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ ℘[L - l₀] 0 = 0

Tactic:
simp [weierstrassPExcept]

Premises used: PeriodPair.weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
trans :
  ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) =
    ℘[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice),
        if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
        else 0
trans₁ :
  (℘[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice),
        if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
        else 0) =
    ℘[L] z
⊢ ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) = ℘[L] z

Tactic:
trans ℘[L - l₀] z + ∑' i : L.lattice, if i = l₀.1 then (1 / (z - l₀.1) ^ 2 - 1 / l₀.1 ^ 2) else 0

Premises used: HSub.hSub, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Subtype.val, PeriodPair.lattice, PeriodPair.weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) =
    ℘[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice),
        if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
        else 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
rw :
  ∑' (b : ↥L.lattice),
      ((if (↑b : ℂ) = (↑l₀ : ℂ) then 0
        else 1 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑b : ℂ) 2) +
        if (↑b : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
        else 0) =
    ℘[L] z
hf :
  Summable (α := ℂ) fun (l : ↥L.lattice) ↦
    if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
hg :
  Summable (α := ℂ) fun (i : ↥L.lattice) ↦
    if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 else 0
⊢ (℘[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice),
        if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
        else 0) =
    ℘[L] z

Tactic:
rw [weierstrassPExcept, ← Summable.tsum_add]

Premises used: Summable.tsum_add, PeriodPair.weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
e_f :
  ∀ (w : ↥L.lattice),
    ((if (↑w : ℂ) = (↑l₀ : ℂ) then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2) +
        if (↑w : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
        else 0) =
      1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2
⊢ ∑' (b : ↥L.lattice),
      ((if (↑b : ℂ) = (↑l₀ : ℂ) then 0
        else 1 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑b : ℂ) 2) +
        if (↑b : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
        else 0) =
    ℘[L] z

Tactic:
congr with w
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
pos :
  (↑w : ℂ) = (↑l₀ : ℂ) →
    0 + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) =
      1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2
neg :
  ¬(↑w : ℂ) = (↑l₀ : ℂ) →
    1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2 + 0 =
      1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2
⊢ ((if (↑w : ℂ) = (↑l₀ : ℂ) then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2) +
      if (↑w : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2
      else 0) =
    1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h : (↑w : ℂ) = (↑l₀ : ℂ)
⊢ 0 + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) =
    1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2

Tactic:
simp only [zero_add, add_zero, *]

Premises used: zero_add, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h : ¬(↑w : ℂ) = (↑l₀ : ℂ)
⊢ 1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2 + 0 =
    1 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑w : ℂ) 2

Tactic:
simp only [zero_add, add_zero, *]

Premises used: zero_add, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable (α := ℂ) fun (l : ↥L.lattice) ↦
    if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2

Tactic:
⟨_, L.hasSum_weierstrassPExcept _ _⟩

Premises used: Exists.intro, PeriodPair.hasSum_weierstrassPExcept, Summable
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable (α := ℂ) fun (l : ↥L.lattice) ↦
    if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2

Tactic:
exact ⟨_, L.hasSum_weierstrassPExcept _ _⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Subset (α := Set ↥L.lattice)
    (Function.support (M := ℂ) fun (i : ↥L.lattice) ↦
      if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 else 0)
    {l₀}

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable (α := ℂ) fun (i : ↥L.lattice) ↦
    if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 else 0

Tactic:
exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

Premises used: Set.Finite.subset, summable_of_hasFiniteSupport, Set.finite_singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
rw :
  ℘[L - (↑l₀ : ℂ)] z =
    ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) +
      (1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2)
⊢ ℘[L - (↑l₀ : ℂ)] z = ℘[L] z + (1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2)

Tactic:
rw [← L.weierstrassPExcept_add l₀]

Premises used: PeriodPair.weierstrassPExcept_add
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - (↑l₀ : ℂ)] z =
    ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) +
      (1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2)

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
h :
  ∀ (z : ℂ) (l : ↥L.lattice),
    (if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) =
      1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
⊢ Eq (α := (z : ℂ) → ℂ)
    (fun (z : ℂ) ↦
      ∑' (l : ↥L.lattice),
        if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    fun (z : ℂ) ↦ ∑' (l : ↥L.lattice), (1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)

Tactic:
congr! 3 with z l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) ∉ L.lattice
⊢ False

Tactic:
simp at hl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
z : ℂ
l : ↥L.lattice
⊢ (↑l : ℂ) ≠ l₀

Tactic:
have : l.1 ≠ l₀ := by rintro rfl; simp at hl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
z : ℂ
l : ↥L.lattice
this : (↑l : ℂ) ≠ l₀
⊢ (if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) =
    1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2

Tactic:
simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦
      if (↑l : ℂ) = L.ω₁ / 2 then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    ℘[L - L.ω₁ / 2]

Tactic:
L.hasSumLocallyUniformly_weierstrassPExcept (L.ω₁ / 2)

Premises used: HDiv.hDiv, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, PeriodPair.ω₁, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
h :
  ∀ (l : ↥L.lattice) (x : ℂ),
    1 / HPow.hPow (β := ℕ) (x - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2 =
      if (↑l : ℂ) = L.ω₁ / 2 then 0 else 1 / HPow.hPow (β := ℕ) (x - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
h₁ : ℘[L] = ℘[L - L.ω₁ / 2]
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) ℘[L]

Tactic:
convert! L.hasSumLocallyUniformly_weierstrassPExcept (L.ω₁ / 2) using 3 with l

Premises used: HDiv.hDiv, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, PeriodPair.ω₁, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
x : ℂ
h : ¬(↑l : ℂ) = L.ω₁ / 2
⊢ 1 / HPow.hPow (β := ℕ) (x - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2 =
    if (↑l : ℂ) = L.ω₁ / 2 then 0 else 1 / HPow.hPow (β := ℕ) (x - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
x : ℂ
⊢ ¬(↑l : ℂ) = L.ω₁ / 2

Tactic:
fun e ↦ L.ω₁_div_two_notMem_lattice (e ▸ l.2)

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, Eq.rec, Not, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
x : ℂ
⊢ ¬(↑l : ℂ) = L.ω₁ / 2

Tactic:
exact fun e ↦ L.ω₁_div_two_notMem_lattice (e ▸ l.2)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
h h₁ : ℘[L] = ℘[L]
⊢ ℘[L] = ℘[L - L.ω₁ / 2]

Tactic:
rw [L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, PeriodPair.weierstrassPExcept_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
⊢ HasSum (fun (l : ↥L.lattice) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) (℘[L] z)

Tactic:
L.hasSumLocallyUniformly_weierstrassP.hasSum

Premises used: PeriodPair.hasSumLocallyUniformly_weierstrassP, HasSumLocallyUniformly.hasSum
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
rw : DifferentiableOn ℂ ℘[L - L.ω₁ / 2] (↑L.lattice : Set ℂ)ᶜ
⊢ DifferentiableOn ℂ ℘[L] (↑L.lattice : Set ℂ)ᶜ

Tactic:
rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, PeriodPair.weierstrassPExcept_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ DifferentiableOn ℂ ℘[L - L.ω₁ / 2] ((↑L.lattice : Set ℂ) \ {L.ω₁ / 2})ᶜ

Tactic:
L.differentiableOn_weierstrassPExcept _

Premises used: PeriodPair.differentiableOn_weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
h : (↑L.lattice : Set ℂ) = (↑L.lattice : Set ℂ) \ {L.ω₁ / 2}
⊢ DifferentiableOn ℂ ℘[L - L.ω₁ / 2] (↑L.lattice : Set ℂ)ᶜ

Tactic:
convert! L.differentiableOn_weierstrassPExcept _

Premises used: PeriodPair.differentiableOn_weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ (↑L.lattice : Set ℂ) = (↑L.lattice : Set ℂ) \ {L.ω₁ / 2}

Tactic:
simp [L.ω₁_div_two_notMem_lattice]

Premises used: PeriodPair.ω₁_div_two_notMem_lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
rw :
  Eq (α := ℂ)
    (∑' (c : ↥L.lattice),
      (1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 2 -
        1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) 2))
    (∑' (l : ↥L.lattice), (1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2))
⊢ Eq (α := ℂ) (∑' (l : ↥L.lattice), (1 / HPow.hPow (β := ℕ) (-z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2))
    (∑' (l : ↥L.lattice), (1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2))

Tactic:
rw [← (Equiv.neg L.lattice).tsum_eq]

Premises used: Equiv.neg, Equiv.tsum_eq, Membership.mem, Subtype, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
e_f :
  ∀ (l : ↥L.lattice),
    1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ)) 2 -
        1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) 2 =
      1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
⊢ Eq (α := ℂ)
    (∑' (c : ↥L.lattice),
      (1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 2 -
        1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) 2))
    (∑' (l : ↥L.lattice), (1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2))

Tactic:
congr with l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
e_f : HPow.hPow (β := ℕ) (-z + (↑l : ℂ)) 2 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2
⊢ 1 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ)) 2 -
      1 / HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) l) : ℂ) 2 =
    1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ HPow.hPow (β := ℕ) (-z + (↑l : ℂ)) 2 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
simp_rw :
  ¬ContinuousAt (Y := ℂ) (fun (z : ℂ) ↦ ℘[L - x] z + (1 / HPow.hPow (β := ℕ) (z - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
⊢ ¬ContinuousAt (Y := ℂ) (fun (z : ℂ) ↦ ℘[L] z) x

Tactic:
simp_rw [← L.weierstrassPExcept_add ⟨x, hx⟩]

Premises used: Subtype.mk, PeriodPair.weierstrassPExcept_add
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
H : ContinuousAt (Y := ℂ) (fun (z : ℂ) ↦ ℘[L - x] z + (1 / HPow.hPow (β := ℕ) (z - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
⊢ ¬(Ne (α := ℂ) 0 0 ∨ LE.le (α := ℤ) 0 (-2))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
H : ContinuousAt (Y := ℂ) (fun (z : ℂ) ↦ ℘[L - x] z + (1 / HPow.hPow (β := ℕ) (z - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
apply : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ HPow.hPow (β := ℤ) x (-2)) 0
⊢ False

Tactic:
apply (NormedField.continuousAt_zpow (n := -2) (x := (0 : ℂ))).not.mpr (by simp)

Premises used: Iff.mpr, Iff.not, NormedField.continuousAt_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
H : ContinuousAt (Y := ℂ) (fun (z : ℂ) ↦ ℘[L - x] z + (1 / HPow.hPow (β := ℕ) (z - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ HPow.hPow (β := ℤ) x (-2)) 0

Tactic:
simpa [Function.comp_def] using
    (((H.sub ((L.differentiableOn_weierstrassPExcept x).differentiableAt
      (L.compl_lattice_diff_singleton_mem_nhds x)).continuousAt).add
      (continuous_const (y := 1 / x ^ 2)).continuousAt).comp_of_eq
      (continuous_const_add x).continuousAt (add_zero _) :)

Premises used: ContinuousAt.add, PeriodPair.compl_lattice_diff_singleton_mem_nhds, continuous_const, ContinuousAt.sub, DifferentiableAt.continuousAt, DifferentiableOn.differentiableAt, Continuous.continuousAt, Function.comp_def, PeriodPair.differentiableOn_weierstrassPExcept, continuous_const_add, ContinuousAt.comp_of_eq, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
refine :
  ∀ (r : ℝ) (hr : r > 0),
    ∀ b ≥ 2 * r,
      ∀ (x : ℂ),
        ‖x‖ < r →
          ∀ (l : ↥L.lattice),
            ‖(↑l : ℂ)‖ = b →
              ‖if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (x - (↑l : ℂ)) 3‖ ≤
                (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦ if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) ℘'[L - l₀]

Tactic:
refine L.hasSumLocallyUniformly_aux (u := fun _ ↦ (16 * ‖·‖ ^ (-3 : ℝ))) _
    (fun _ _ ↦ (ZLattice.summable_norm_rpow _ _ (by simp; norm_num)).mul_left _) fun r hr ↦
    Filter.eventually_atTop.mpr ⟨2 * r, ?_⟩

Premises used: Iff.mpr, Norm.norm, HMul.hMul, ZLattice.summable_norm_rpow, Summable.mul_left, HPow.hPow, Exists.intro, PeriodPair.hasSumLocallyUniformly_aux, Filter.eventually_atTop, OfNat.ofNat, PeriodPair.lattice, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
pos : (↑l : ℂ) = l₀ → norm (E := ℂ) 0 ≤ (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
neg :
  ¬(↑l : ℂ) = l₀ →
    ‖-2 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 3‖ ≤
      (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
⊢ ‖if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 3‖ ≤
    (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l

Tactic:
split_ifs