awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
h : ‖(↑p.2 : ℂ) - x‖ = 0
hx₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
hκ'₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ * κ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
⊢ Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - (↑p.2 : ℂ)‖ (-3) * ‖z - (↑p.2 : ℂ)‖

Tactic:
obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h

Premises used: Prod.snd, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
h : ‖(↑p.2 : ℂ) - x‖ = 0
hx₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
hκ'₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ * κ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
H₃ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - (↑p.2 : ℂ)‖ (-3) * ‖z - (↑p.2 : ℂ)‖
⊢ ‖(↑p.2 : ℂ) - (↑p.2 : ℂ)‖ = 0

Tactic:
obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h

Premises used: Prod.snd, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
κ : ℝ
hκ : 1 < κ
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ * κ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - (↑p.2 : ℂ)‖ (-3) * ‖z - (↑p.2 : ℂ)‖
h : ‖(↑p.2 : ℂ) - (↑p.2 : ℂ)‖ = 0
⊢ False

Tactic:
simpa [(norm_nonneg _).not_gt] using hx p.2 hp

Premises used: LE.le.not_gt, Prod.snd, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
⊢ ‖(↑p.2 : ℂ) - x‖ ≠ 0

Tactic:
have hpx : ‖p.2 - x‖ ≠ 0 := fun h ↦ by
      obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h
      simpa [(norm_nonneg _).not_gt] using hx p.2 hp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
neg :
  ∀ (hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - z‖ < ‖(↑l : ℂ) - z‖)
    (hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - z‖ * κ < ‖(↑l : ℂ) - z‖)
    (H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - z‖ (-3) * ‖z - z‖)
    (hpx : ‖(↑p.2 : ℂ) - z‖ ≠ 0),
    ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - z) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
          (z - z) ^ (p.1 + 1)‖ ≤
      HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
        (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - z‖ (-3) * ‖z - z‖)
neg₁ :
  ∀ (hxz : z ≠ x),
    ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
          (z - x) ^ (p.1 + 1)‖ ≤
      HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
        (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
⊢ ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)

Tactic:
obtain rfl | hxz := eq_or_ne z x

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
κ : ℝ
hκ : 1 < κ
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - z‖ < ‖(↑l : ℂ) - z‖
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - z‖ * κ < ‖(↑l : ℂ) - z‖
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - z‖ (-3) * ‖z - z‖
hpx : ‖(↑p.2 : ℂ) - z‖ ≠ 0
⊢ ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - z) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - z) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - z‖ (-3) * ‖z - z‖)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
norm_num :
  ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 1 + 1‖ * ‖(↑p.2 : ℂ) - x‖ ^ (-2 + HAdd.hAdd (α := ℤ) (-1) (-(↑p.1 : ℤ))) =
      ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ‖(↑p.2 : ℂ) - x‖ ^ HSub.hSub (α := ℤ) (-3) (↑p.1 : ℤ) ∨
    z - x = 0
⊢ ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ =
    ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ‖(↑p.2 : ℂ) - x‖ ^ HSub.hSub (α := ℤ) (-3) (↑p.1 : ℤ) * ‖z - x‖ ^ (p.1 + 1)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
ring_nf : True ∨ -x + z = 0
⊢ ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 1 + 1‖ * ‖(↑p.2 : ℂ) - x‖ ^ (-2 + HAdd.hAdd (α := ℤ) (-1) (-(↑p.1 : ℤ))) =
      ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ‖(↑p.2 : ℂ) - x‖ ^ HSub.hSub (α := ℤ) (-3) (↑p.1 : ℤ) ∨
    z - x = 0

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
⊢ True ∨ -x + z = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
simp :
  ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ((HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ / ‖(↑p.2 : ℂ) - x‖ ^ p.1) *
      ‖z - x‖ ^ (p.1 + 1) =
    ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * (‖z - x‖ ^ p.1 / ‖(↑p.2 : ℂ) - x‖ ^ p.1) *
      ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)
⊢ ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ‖(↑p.2 : ℂ) - x‖ ^ HSub.hSub (α := ℤ) (-3) (↑p.1 : ℤ) * ‖z - x‖ ^ (p.1 + 1) =
    ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ((‖(↑p.2 : ℂ) - x‖ / ‖z - x‖) ^ p.1)⁻¹ *
      ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)

Tactic:
simp [hpx, zpow_sub₀, div_pow]

Premises used: zpow_sub₀, div_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ((HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ / ‖(↑p.2 : ℂ) - x‖ ^ p.1) *
      ‖z - x‖ ^ (p.1 + 1) =
    ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * (‖z - x‖ ^ p.1 / ‖(↑p.2 : ℂ) - x‖ ^ p.1) *
      ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
hbc : ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ ≤ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2
hbc₁ : κ ≤ ‖(↑p.2 : ℂ) - x‖ / ‖z - x‖
⊢ ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ((‖(↑p.2 : ℂ) - x‖ / ‖z - x‖) ^ p.1)⁻¹ *
      ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖) ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * (κ ^ p.1)⁻¹ * ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
hbc hbc₁ hbc₂ hbc₃ : p.1 + 2 ≤ p.1 + 2
⊢ ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ ≤ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
⊢ 0 < ‖z - x‖

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
⊢ κ ≤ ‖(↑p.2 : ℂ) - x‖ / ‖z - x‖

Tactic:
exact (le_div_iff₀ (by simpa [sub_eq_zero])).mpr ((mul_comm _ _).trans_le (hκ' p.2 hp).le)

Premises used: Iff.mpr, LT.lt.le, Eq.trans_le, mul_comm, le_div_iff₀, Prod.snd
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
⊢ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * (κ ^ p.1)⁻¹ * ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖) =
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)

Tactic:
simp [zpow_ofNat]

Premises used: zpow_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
hpx : ‖(↑p.2 : ℂ) - x‖ ≠ 0
hxz : z ≠ x
_ :
  ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ =
    ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ‖(↑p.2 : ℂ) - x‖ ^ HSub.hSub (α := ℤ) (-3) (↑p.1 : ℤ) * ‖z - x‖ ^ (p.1 + 1)
_₁ :
  ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ‖(↑p.2 : ℂ) - x‖ ^ HSub.hSub (α := ℤ) (-3) (↑p.1 : ℤ) * ‖z - x‖ ^ (p.1 + 1) =
    ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ((‖(↑p.2 : ℂ) - x‖ / ‖z - x‖) ^ p.1)⁻¹ *
      ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)
_₂ :
  ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ((‖(↑p.2 : ℂ) - x‖ / ‖z - x‖) ^ p.1)⁻¹ *
      ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖) ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * (κ ^ p.1)⁻¹ * ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)
_₃ :
  HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * (κ ^ p.1)⁻¹ * ((HPow.hPow (β := ℕ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖) =
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
⊢ ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)

Tactic:
calc
      _ = ‖(p.1 + 2 : ℂ)‖ * ‖p.2 - x‖ ^ (-3 - p.1 : ℤ) * ‖z - x‖ ^ (p.1 + 1) := by
        norm_num; ring_nf; simp
      _ = ‖(p.1 + 2 : ℂ)‖ * ((‖↑p.2 - x‖ / ‖z - x‖) ^ p.1)⁻¹ * ((‖p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖) := by
        simp [hpx, zpow_sub₀, div_pow]; field
      _ ≤ (p.1 + 2) * (κ ^ p.1)⁻¹ * ((‖p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖) := by
        gcongr
        · norm_cast
        · exact (le_div_iff₀ (by simpa [sub_eq_zero])).mpr ((mul_comm _ _).trans_le (hκ' p.2 hp).le)
      _ = _ := by simp [zpow_ofNat]

Premises used: Norm.norm, HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.cast, Prod.fst, Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Subtype.val, Prod.snd, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
trans :
  ℘[L - l₀] z =
    ∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i
trans₁ :
  Eq (α := ℂ)
    (∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i)
    (∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i)
⊢ ℘[L - l₀] z = ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
trans ∑' (l : L.lattice) (i : ℕ), if l.1 = l₀ then 0 else
      ((i + 1) * (l.1 - x) ^ (- ↑(i + 2) : ℤ) - i.casesOn (l.1 ^ (-2 : ℤ)) 0) * (z - x) ^ i

Premises used: HSub.hSub, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
e_f :
  ∀ (l : ↥L.lattice),
    (if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) =
      ∑' (i : ℕ),
        if (↑l : ℂ) = l₀ then 0
        else
          HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
              (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
            (z - x) ^ i
⊢ Eq (α := ℂ)
    (∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    (∑' (l : ↥L.lattice) (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i)

Tactic:
congr 1 with l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
l : ↥L.lattice
pos : ∀ (h : (↑l : ℂ) = l₀), Eq (α := ℂ) 0 (∑' (i : ℕ), 0)
neg :
  ∀ (h : ¬(↑l : ℂ) = l₀),
    1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2 =
      ∑' (i : ℕ),
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i
⊢ (if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) =
    ∑' (i : ℕ),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
          (z - x) ^ i

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
l : ↥L.lattice
h : (↑l : ℂ) = l₀
⊢ Eq (α := ℂ) 0 (∑' (i : ℕ), 0)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
l : ↥L.lattice
h : ¬(↑l : ℂ) = l₀
⊢ (↑l : ℂ) ≠ x

Tactic:
simpa [sub_eq_zero] using (norm_nonneg _).trans_lt (hx l h)

Premises used: sub_eq_zero, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
l : ↥L.lattice
h : ¬(↑l : ℂ) = l₀
⊢ Membership.mem (γ := Set ℂ) (Metric.eball 0 ‖(↑l : ℂ) - x‖ₑ) (z - x)

Tactic:
simpa [enorm_eq_nnnorm] using hx _ h

Premises used: enorm_eq_nnnorm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
l : ↥L.lattice
h : ¬(↑l : ℂ) = l₀
⊢ 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2 =
    ∑' (i : ℕ),
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ) *
        (z - x) ^ i

Tactic:
simpa [mul_comm] using ((Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero l x
      (by simpa [sub_eq_zero] using (norm_nonneg _).trans_lt (hx l h))).hasSum (y := z - x)
      (by simpa [enorm_eq_nnnorm] using hx _ h)).tsum_eq.symm

Premises used: HasFPowerSeriesOnBall.hasSum, HasSum.tsum_eq, mul_comm, Eq.symm, Subtype.val, Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero