awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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
⊢ False
have hx₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
Tactic: obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h
Cleared hypotheses: x, hx, hκ', H₂, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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 : ℂ)‖
⊢ False
have hκ'₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ * κ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
Tactic: obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h
Cleared hypotheses: x, hx, hκ', H₂, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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 : ℂ)‖
⊢ False
have H₃ : 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
Cleared hypotheses: x, hx, hκ', H₂, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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 : ℂ)‖
⊢ False
have h₁ : ‖(↑p.2 : ℂ) - (↑p.2 : ℂ)‖ = 0
Tactic: obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h
Cleared hypotheses: x, hx, hκ', H₂, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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₀
⊢ ‖(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‖)
have hpx : ‖(↑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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ‖(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‖)
have 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‖)
Tactic: obtain rfl | hxz := eq_or_ne z x
Cleared hypotheses: x, hx, hκ', H₂, hpx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖)
⊢ ‖(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‖)
have 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‖)
Tactic: obtain rfl | hxz := eq_or_ne z x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
have 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
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖ ^ (-2 + HAdd.hAdd (α := ℤ) (-1) (-(↑p.1 : ℤ))) =
      ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ * ‖(↑p.2 : ℂ) - x‖ ^ HSub.hSub (α := ℤ) (-3) (↑p.1 : ℤ) ∨
    z - x = 0
have ring_nf : True ∨ -x + z = 0
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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.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‖)
have 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‖)
Tactic: simp [hpx, zpow_sub₀, div_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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.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‖)
have hbc : ‖HAdd.hAdd (α := ℂ) (↑p.1 : ℂ) 2‖ ≤ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ‖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‖)
have hbc₁ : κ ≤ ‖(↑p.2 : ℂ) - x‖ / ‖z - x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖ ≤ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2
have hbc : p.1 + 2 ≤ p.1 + 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
have _ : ‖(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: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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 + 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‖)
have _₁ : ‖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: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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 + 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‖)
have _₂ : ‖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: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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 + 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‖)
have _₃ : 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: 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]