awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ ¬(↑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.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

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

Tactic:
L.hasSumLocallyUniformly_derivWeierstrassP.tendstoLocallyUniformlyOn.tendsto_at (Set.mem_univ z)

Premises used: iInf, PeriodPair.hasSumLocallyUniformly_derivWeierstrassP, TendstoLocallyUniformly.tendstoLocallyUniformlyOn, Filter.atTop, TendstoLocallyUniformlyOn.tendsto_at, HasSum, Set.mem_univ
-- 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.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

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

Tactic:
L.differentiableOn_derivWeierstrassPExcept _

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

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 : ℂ
simp :
  Eq (α := ℂ) (∑' (b : ↥L.lattice), 2 / -HPow.hPow (β := ℕ) ((↑b : ℂ) - z) 3)
    (∑' (b : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
⊢ Eq (α := ℂ)
    (-∑' (c : ↥L.lattice),
        2 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
    (- -∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)

Tactic:
simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub, neg_neg,
    ← div_neg, ← tsum_neg]

Premises used: neg_add_eq_sub, neg_neg, Equiv.neg_apply, div_neg, tsum_neg, sub_neg_eq_add, NegMemClass.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
h : ∀ (l : ↥L.lattice), -HPow.hPow (β := ℕ) ((↑l : ℂ) - z) 3 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
⊢ Eq (α := ℂ) (∑' (b : ↥L.lattice), 2 / -HPow.hPow (β := ℕ) ((↑b : ℂ) - z) 3)
    (∑' (b : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)

Tactic:
congr! with l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -HPow.hPow (β := ℕ) ((↑l : ℂ) - z) 3 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
rw :
  Eq (α := ℂ)
    (-∑' (c : ↥L.lattice),
        2 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑((Equiv.addRight l : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
    (-∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
⊢ Eq (α := ℂ) (-∑' (l_1 : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l_1 : ℂ)) 3)
    (-∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)

Tactic:
rw [← (Equiv.addRight l).tsum_eq]

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

Tactic:
simp only [← tsum_neg, ← div_neg, Equiv.coe_addRight, Submodule.coe_add, add_sub_add_right_eq_sub]

Premises used: Submodule.coe_add, Equiv.coe_addRight, div_neg, tsum_neg, add_sub_add_right_eq_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
⊢ Function.Periodic ℘'[L] (↑l : ℂ)

Tactic:
(L.derivWeierstrassP_add_coe · l)

Premises used: Function.Periodic, PeriodPair.derivWeierstrassP_add_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
rw : ℘'[L] 0 = -℘'[L] 0
rw₁ : ℘'[L] 0 = ℘'[L] (-0)
rw₂ rw₃ : ℘'[L] 0 = ℘'[L] 0
⊢ ℘'[L] 0 = 0

Tactic:
rw [← CharZero.eq_neg_self_iff, ← L.derivWeierstrassP_neg, neg_zero]

Premises used: PeriodPair.derivWeierstrassP_neg, CharZero.eq_neg_self_iff, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
rw : ℘'[L] (0 + (↑l : ℂ)) = 0
rw₁ : ℘'[L] 0 = 0
rw₂ rw₃ : Eq (α := ℂ) 0 0
⊢ ℘'[L] (↑l : ℂ) = 0

Tactic:
rw [← zero_add l.1, L.derivWeierstrassP_add_coe, L.derivWeierstrassP_zero]

Premises used: zero_add, Subtype.val, PeriodPair.derivWeierstrassP_add_coe, PeriodPair.derivWeierstrassP_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
rw : ℘'[L] (z - (↑l : ℂ) + (↑l : ℂ)) = ℘'[L] z
rw₁ rw₂ : ℘'[L] z = ℘'[L] z
⊢ ℘'[L] (z - (↑l : ℂ)) = ℘'[L] z

Tactic:
rw [← L.derivWeierstrassP_add_coe _ l, sub_add_cancel]

Premises used: sub_add_cancel, PeriodPair.derivWeierstrassP_add_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
h : ∀ (x : ℂ), deriv ℘[L] x = ℘'[L] x
⊢ deriv ℘[L] = ℘'[L]

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
pos : ∀ (hx : x ∈ L.lattice), deriv ℘[L] x = ℘'[L] x
neg : ∀ (hx : x ∉ L.lattice), deriv ℘[L] x = ℘'[L] x
⊢ deriv ℘[L] x = ℘'[L] x

Tactic:
by_cases hx : x ∈ L.lattice

Premises used: PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
pos : ¬DifferentiableAt ℂ ℘[L] x
⊢ deriv ℘[L] x = ℘'[L] x

Tactic:
rw [deriv_zero_of_not_differentiableAt, L.derivWeierstrassP_coe ⟨x, hx⟩]

Premises used: deriv_zero_of_not_differentiableAt, Subtype.mk, PeriodPair.derivWeierstrassP_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬DifferentiableAt ℂ ℘[L] x

Tactic:
fun H ↦ L.not_continuousAt_weierstrassP x hx H.continuousAt

Premises used: DifferentiableAt.continuousAt, PeriodPair.not_continuousAt_weierstrassP, Not
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬DifferentiableAt ℂ ℘[L] x

Tactic:
exact fun H ↦ L.not_continuousAt_weierstrassP x hx H.continuousAt

Premises used: PeriodPair.not_continuousAt_weierstrassP
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ x ∈ ((↑L.lattice : Set ℂ) \ {L.ω₁ / 2})ᶜ

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
neg : deriv ℘[L - L.ω₁ / 2] x = ℘'[L] x
neg₁ : deriv ℘[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x
neg₂ neg₃ : ℘'[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x
⊢ deriv ℘[L] x = ℘'[L] x

Tactic:
rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      ← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L.ω₁ / 2) (x := x) (by simp [hx])]

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, PeriodPair.derivWeierstrassPExcept_of_notMem, HDiv.hDiv, PeriodPair.ω₁, OfNat.ofNat, PeriodPair.weierstrassPExcept_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
⊢ LT.lt (α := ℤ) (-(↑r : ℤ)) (-(↑(finrank ℤ ↥L.lattice) : ℤ))

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
refine : ∀ (l : ↥L.lattice), ‖(((↑l : ℂ) - x) ^ r)⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
⊢ HasSum (fun (l : ↥L.lattice) ↦ (((↑l : ℂ) - x) ^ r)⁻¹) (L.sumInvPow x r)

Tactic:
refine Summable.hasSum (.of_norm_bounded (ZLattice.summable_norm_sub_zpow _
    (-r) (by simpa) x) fun l ↦ ?_)

Premises used: Nat.cast, Summable.hasSum, Summable.of_norm_bounded, ZLattice.summable_norm_sub_zpow, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
rw : ‖(HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (↑r : ℤ))⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
rw₁ : ‖HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑r : ℤ))‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))
rw₂ rw₃ : ‖HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑r : ℤ))‖ ≤ ‖HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑r : ℤ))‖
⊢ ‖(((↑l : ℂ) - x) ^ r)⁻¹‖ ≤ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-(↑r : ℤ))

Tactic:
rw [← zpow_natCast, ← zpow_neg, ← norm_zpow]

Premises used: zpow_natCast, zpow_neg, norm_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
⊢ 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:
simp [weierstrassPExcept, sub_sq_comm x, zpow_ofNat]

Premises used: sub_sq_comm, zpow_ofNat, PeriodPair.weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
pos :
  ∀ (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) - ((l₀ - x) ^ (i + 2))⁻¹))
        (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 : ℂ)
neg :
  ∀ (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 : ℂ)
⊢ 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:
split_ifs with hl₀
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
trans :
  FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (i + 1) =
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0)
trans₁ :
  HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0) =
    ∑' (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 : ℂ)
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (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:
trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)

Premises used: HSub.hSub, Nat.cast, Subtype.mk, HPow.hPow, HAdd.hAdd, tsum, OfNat.ofNat, Eq, Neg.neg, SummationFilter.unconditional, PeriodPair.sumInvPow, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
rw :
  (if i + 1 = 0 then ℘[L - l₀] x
    else HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ (i + 3))⁻¹)
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹))
      (i + 1) =
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0)

Tactic:
rw [FormalMultilinearSeries.coeff_ofScalars, tsum_ite_eq, zpow_neg, zpow_natCast]

Premises used: zpow_natCast, FormalMultilinearSeries.coeff_ofScalars, zpow_neg, tsum_ite_eq, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x
    else HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ (i + 3))⁻¹)

Tactic:
simp [add_assoc, one_add_one_eq_two]

Premises used: add_assoc, one_add_one_eq_two
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
linarith : i + 3 ≤ 2 → -1 + HSub.hSub (α := ℤ) 0 (↑i : ℤ) + (HAdd.hAdd (α := ℤ) (↑i : ℤ) 3 - 2) = 0
⊢ 2 < i + 3

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
rw :
  Eq (α := ℂ)
    (∑' (x_1 : ↥L.lattice),
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
        ((((↑x_1 : ℂ) - x) ^ (i + 3))⁻¹ -
          if x_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then
            HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0))
    (∑' (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 : ℂ))
rw₁ :
  Summable (α := ℂ) fun (l : ↥L.lattice) ↦
    if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
    else 0
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
      (L.sumInvPow x (i + 3) -
        ∑' (l : ↥L.lattice),
          if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0) =
    ∑' (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:
rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]

Premises used: tsum_mul_left, HasSum.summable, PeriodPair.hasSum_sumInvPow, Summable.tsum_sub, PeriodPair.sumInvPow
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
simp_rw :
  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)
⊢ Eq (α := ℂ)
    (∑' (x_1 : ↥L.lattice),
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 *
        ((((↑x_1 : ℂ) - x) ^ (i + 3))⁻¹ -
          if x_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then
            HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
          else 0))
    (∑' (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:
simp_rw [Subtype.ext_iff, zpow_neg]

Premises used: Subtype.ext_iff, zpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
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
⊢ 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)

Tactic:
congr with l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
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
⊢ 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:
split_ifs with e
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : (↑l : ℂ) = l₀
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - (HPow.hPow (β := ℤ) (l₀ - x) (↑(i + 3) : ℤ))⁻¹) = 0

Tactic:
simp only [e, zpow_natCast, sub_self, mul_zero]

Premises used: zpow_natCast, sub_self, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬(↑l : ℂ) = l₀
neg : (↑(i + 2) : ℂ) * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1 + 1) : ℂ) * (((↑l : ℂ) - x) ^ (i + 1 + 2))⁻¹ - 0
⊢ HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - 0) =
    HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * (((↑l : ℂ) - x) ^ (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 + 2))⁻¹ - 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬(↑l : ℂ) = l₀
⊢ (↑(i + 2) : ℂ) * ((((↑l : ℂ) - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1 + 1) : ℂ) * (((↑l : ℂ) - x) ^ (i + 1 + 2))⁻¹ - 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Subset (α := Set ↥L.lattice)
    (Function.support (M := ℂ) fun (l : ↥L.lattice) ↦
      if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
      else 0)
    {Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀}

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Summable (α := ℂ) fun (l : ↥L.lattice) ↦
    if l = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀ then HPow.hPow (β := ℤ) (l₀ - x) (-(↑(i + 3) : ℤ))
    else 0

Tactic:
exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))

Premises used: Set.Finite.subset, summable_of_hasFiniteSupport, Set.finite_singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
⊢ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀

Tactic:
have h₁ (l : L.lattice) : l.1 ≠ l₀ := fun e ↦ hl₀ (e ▸ l.2)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
h₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀
⊢ 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 : ℂ)

Tactic:
simp [h₁, tsum_mul_left, sumInvPow, add_assoc,
        one_add_one_eq_two, ← zpow_natCast, -neg_add_rev]

Premises used: neg_add_rev, zpow_natCast, add_assoc, tsum_mul_left, one_add_one_eq_two, PeriodPair.sumInvPow
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Membership.mem (γ := Set ℝ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ) 1

Tactic:
simpa [Complex.dist_eq, @forall_comm ℝ, norm_sub_rev x] using hx

Premises used: forall_comm, Complex.dist_eq, norm_sub_rev