awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ℘[L - (↑l₀ : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2) = ℘[L] z
have 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
Tactic: trans ℘[L - l₀] z + ∑' i : L.lattice, if i = l₀.1 then (1 / (z - l₀.1) ^ 2 - 1 / l₀.1 ^ 2) else 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ (℘[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
have 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
Tactic: rw [weierstrassPExcept, ← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ (℘[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
have hf : Summable (α := ℂ) fun (l : ↥L.lattice) ↦
  if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2
Tactic: rw [weierstrassPExcept, ← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ (℘[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
have hg : Summable (α := ℂ) fun (i : ↥L.lattice) ↦
  if (↑i : ℂ) = (↑l₀ : ℂ) then 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 else 0
Tactic: rw [weierstrassPExcept, ← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ∑' (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
have 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
Tactic: congr with w
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ((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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - (↑l₀ : ℂ)] z = ℘[L] z + (1 / HPow.hPow (β := ℕ) (↑l₀ : ℂ) 2 - 1 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 2)
have 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)
Tactic: rw [← L.weierstrassPExcept_add l₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ 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)
have 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
Tactic: congr! 3 with z l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
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
have this : (↑l : ℂ) ≠ l₀
Tactic: have : l.1 ≠ l₀ := by rintro rfl; simp at hl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) ℘[L]
have 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
Tactic: convert! L.hasSumLocallyUniformly_weierstrassPExcept (L.ω₁ / 2) using 3 with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2) ℘[L]
have h₁ : ℘[L] = ℘[L - L.ω₁ / 2]
Tactic: convert! L.hasSumLocallyUniformly_weierstrassPExcept (L.ω₁ / 2) using 3 with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
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
have h : ¬(↑l : ℂ) = L.ω₁ / 2
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ ℘[L] = ℘[L - L.ω₁ / 2]
have h : ℘[L] = ℘[L]
Tactic: rw [L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ DifferentiableOn ℂ ℘[L] (↑L.lattice : Set ℂ)ᶜ
have rw : DifferentiableOn ℂ ℘[L - L.ω₁ / 2] (↑L.lattice : Set ℂ)ᶜ
Tactic: rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ DifferentiableOn ℂ ℘[L - L.ω₁ / 2] (↑L.lattice : Set ℂ)ᶜ
have h : (↑L.lattice : Set ℂ) = (↑L.lattice : Set ℂ) \ {L.ω₁ / 2}
Tactic: convert! L.differentiableOn_weierstrassPExcept _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
⊢ 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))
have 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))
Tactic: rw [← (Equiv.neg L.lattice).tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
⊢ 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))
have 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
Tactic: congr with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
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
have e_f : HPow.hPow (β := ℕ) (-z + (↑l : ℂ)) 2 = HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬ContinuousAt (Y := ℂ) (fun (z : ℂ) ↦ ℘[L] z) x
have simp_rw : ¬ContinuousAt (Y := ℂ) (fun (z : ℂ) ↦ ℘[L - x] z + (1 / HPow.hPow (β := ℕ) (z - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
Tactic: simp_rw [← L.weierstrassPExcept_add ⟨x, hx⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ False
have apply : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ HPow.hPow (β := ℤ) x (-2)) 0
Tactic: apply (NormedField.continuousAt_zpow (n := -2) (x := (0 : ℂ))).not.mpr (by simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦ if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) ℘'[L - l₀]
have 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
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, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
⊢ ‖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
have pos : (↑l : ℂ) = l₀ → norm (E := ℂ) 0 ≤ (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ‖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
have neg : ¬(↑l : ℂ) = l₀ →
  ‖-2 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 3‖ ≤ (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
hs : ‖(↑l : ℂ)‖ < r
⊢ False
have linarith : 0 - r + (2 * r - ‖(↑l : ℂ)‖) + (‖(↑l : ℂ)‖ - r) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
⊢ ‖-2 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 3‖ ≤ (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
have this : s ≠ (↑l : ℂ)
Tactic: have : s ≠ ↑l := by rintro rfl; exfalso; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
h : norm (E := ℂ) (↑0 : ℂ) ≥ 2 * r
h_1 : ¬(↑0 : ℂ) = l₀
this : s ≠ (↑0 : ℂ)
⊢ False
have hr₁ : 0 < r
Tactic: simp_all
Cleared hypotheses: hr, hs, h, h_1, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
h : norm (E := ℂ) (↑0 : ℂ) ≥ 2 * r
h_1 : ¬(↑0 : ℂ) = l₀
this : s ≠ (↑0 : ℂ)
hr₁ : 0 < r
hs₁ : ‖s‖ < r
⊢ False
have h₁ : 2 * r ≤ 0
Tactic: simp_all
Cleared hypotheses: hr, hs, h, h_1, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
h : norm (E := ℂ) (↑0 : ℂ) ≥ 2 * r
h_1 : ¬(↑0 : ℂ) = l₀
this : s ≠ (↑0 : ℂ)
hr₁ : 0 < r
hs₁ : ‖s‖ < r
h₁ : 2 * r ≤ 0
⊢ False
have h₂ : ¬0 = l₀
Tactic: simp_all
Cleared hypotheses: hr, hs, h, h_1, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
h : norm (E := ℂ) (↑0 : ℂ) ≥ 2 * r
h_1 : ¬(↑0 : ℂ) = l₀
this : s ≠ (↑0 : ℂ)
hr₁ : 0 < r
hs₁ : ‖s‖ < r
h₁ : 2 * r ≤ 0
h₂ : ¬0 = l₀
⊢ False
have this₁ : ¬s = 0
Tactic: simp_all
Cleared hypotheses: hr, hs, h, h_1, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hr : 0 < r
hs : ‖s‖ < r
h : 2 * r ≤ 0
h_1 : ¬0 = l₀
this : ¬s = 0
⊢ False
have linarith : 2 * (0 - r) + (2 * r - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hr : 0 < r
hs : ‖s‖ < r
h : 2 * r ≤ 0
h_1 : ¬0 = l₀
this : ¬s = 0
linarith : 2 * (0 - r) + (2 * r - 0) = 0
⊢ False
have linarith₁ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this : s ≠ (↑l : ℂ)
⊢ ‖-2 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 3‖ ≤ (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
have this₁ : l ≠ 0
Tactic: have : l ≠ 0 := by rintro rfl; simp_all; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ ‖-2 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 3‖ ≤ (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l
have neg : 2 / HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3 ≤ 16 * HPow.hPow (β := ℝ) ‖l‖ (-3)
Tactic: simp only [Complex.norm_div, norm_neg, Complex.norm_ofNat, norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 2 / HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3 ≤ 16 * HPow.hPow (β := ℝ) ‖l‖ (-3)
have neg : 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 16 * HPow.hPow (β := ℕ) ‖(↑l : ℂ) - s‖ 3
Tactic: rw [Real.rpow_neg (by positivity), ← div_eq_mul_inv, div_le_div_iff₀, norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 16 * HPow.hPow (β := ℕ) ‖(↑l : ℂ) - s‖ 3
⊢ 2 / HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3 ≤ 16 * HPow.hPow (β := ℝ) ‖l‖ (-3)
have neg₁ : 0 < HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3
Tactic: rw [Real.rpow_neg (by positivity), ← div_eq_mul_inv, div_le_div_iff₀, norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 16 * HPow.hPow (β := ℕ) ‖(↑l : ℂ) - s‖ 3
neg₁ : 0 < HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3
⊢ 2 / HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3 ≤ 16 * HPow.hPow (β := ℝ) ‖l‖ (-3)
have neg₂ : 0 < HPow.hPow (β := ℝ) ‖l‖ 3
Tactic: rw [Real.rpow_neg (by positivity), ← div_eq_mul_inv, div_le_div_iff₀, norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 16 * HPow.hPow (β := ℕ) ‖(↑l : ℂ) - s‖ 3
have neg : 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3
Tactic: refine LE.le.trans_eq (b := 2 * (2 * ‖l - s‖) ^ 3) ?_ (by ring)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3
have neg : 2 * HPow.hPow (β := ℕ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 2 * HPow.hPow (β := ℕ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3
have neg : ‖l‖ ≤ 2 * ‖(↑l : ℂ) - s‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 0 ≤ ‖(↑l : ℂ)‖ - ‖s‖
have linarith : ‖(↑l : ℂ)‖ - ‖s‖ < 0 → 0 - r + (‖s‖ - r) + (2 * r - ‖(↑l : ℂ)‖) + (‖(↑l : ℂ)‖ - ‖s‖ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ LE.le (α := ℝ) 0 2
have linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
⊢ LE.le (α := ℝ) 0 2
have linarith₁ : LT.lt (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ ‖l‖ ≤ 2 * ‖(↑l : ℂ) - s‖
have neg : ‖l‖ ≤ 2 * (‖(↑l : ℂ)‖ - ‖s‖)
Tactic: refine le_trans ?_ (mul_le_mul le_rfl (norm_sub_norm_le _ _) (by linarith) (by linarith))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ ‖l‖ ≤ 2 * (‖(↑l : ℂ)‖ - ‖s‖)
have neg : ∀ (hr : r > 0), ‖l‖ ≤ 2 * (‖l‖ - ‖s‖)
Tactic: norm_cast at *
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖l‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : ¬s = (↑l : ℂ)
this : ¬l = 0
hr : r > 0
⊢ ‖l‖ ≤ 2 * (‖l‖ - ‖s‖)
have linarith : 2 * (‖l‖ - ‖s‖) < ‖l‖ → 2 * (‖s‖ - r) + (2 * r - ‖l‖) + (2 * (‖l‖ - ‖s‖) - ‖l‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖l‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
this_1 : ¬s = (↑l : ℂ)
this : ¬l = 0
hr : r > 0
linarith : 2 * (‖l‖ - ‖s‖) < ‖l‖ → 2 * (‖s‖ - r) + (2 * r - ‖l‖) + (2 * (‖l‖ - ‖s‖) - ‖l‖) = 0
⊢ ‖l‖ ≤ 2 * (‖l‖ - ‖s‖)
have linarith₁ : 2 * (‖l‖ - ‖s‖) < ‖l‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith