awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
refine : ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (Metric.ball 0 r)

Tactic:
refine tendstoUniformlyOn_tsum_of_cofinite_eventually (hu r hr) ?_

Premises used: tendstoUniformlyOn_tsum_of_cofinite_eventually
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
obtain :
  ∀ (R : ℝ) (hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l),
    ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n
⊢ ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n

Tactic:
obtain ⟨R, hR⟩ := eventually_atTop.mp (hf r hr)

Premises used: Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
⊢ ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n

Tactic:
(isCompact_iff_finite.mp (isCompact_closedBall (0 : L.lattice) R)).subset ?_

Premises used: isCompact_iff_finite, Set.Mem, Filter.Eventually, setOf, Set.Finite, Set.Finite.subset, Iff.mp, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
refine :
  Subset (α := Set ↥L.lattice)
    {x : ↥L.lattice |
        (fun (n : ↥L.lattice) ↦ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n) x}ᶜ
    (Metric.closedBall 0 R)
⊢ ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n

Tactic:
refine (isCompact_iff_finite.mp (isCompact_closedBall (0 : L.lattice) R)).subset ?_

Premises used: isCompact_iff_finite, Set.Finite.subset, Iff.mp, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl :
  Membership.mem (γ := Set ↥L.lattice)
    {x : ↥L.lattice |
        (fun (n : ↥L.lattice) ↦ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n) x}ᶜ
    l
⊢ ∃ (x : ℂ), ‖x‖ < r ∧ u r l < ‖f l x‖

Tactic:
simpa using hl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl :
  Membership.mem (γ := Set ↥L.lattice)
    {x : ↥L.lattice |
        (fun (n : ↥L.lattice) ↦ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n) x}ᶜ
    l
obtain :
  ∀ (s : ℂ) (hs : ‖s‖ < r) (hs' : u r l < ‖f l s‖), Membership.mem (γ := Set ↥L.lattice) (Metric.closedBall 0 R) l
⊢ Membership.mem (γ := Set ↥L.lattice) (Metric.closedBall 0 R) l

Tactic:
obtain ⟨s, hs, hs'⟩ : ∃ x, ‖x‖ < r ∧ u r l < ‖f l x‖ := by simpa using hl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl :
  Membership.mem (γ := Set ↥L.lattice)
    {x : ↥L.lattice |
        (fun (n : ↥L.lattice) ↦ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n) x}ᶜ
    l
s : ℂ
hs : ‖s‖ < r
hs' : u r l < ‖f l s‖
simp : ‖l‖ ≤ R
⊢ Membership.mem (γ := Set ↥L.lattice) (Metric.closedBall 0 R) l

Tactic:
simp only [Metric.mem_closedBall, dist_zero_right]

Premises used: Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl :
  Membership.mem (γ := Set ↥L.lattice)
    {x : ↥L.lattice |
        (fun (n : ↥L.lattice) ↦ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n) x}ᶜ
    l
s : ℂ
hs : ‖s‖ < r
hs' : u r l < ‖f l s‖
contrapose! : ∀ (hs' : R < ‖l‖), ‖f l s‖ ≤ u r l
⊢ ‖l‖ ≤ R

Tactic:
contrapose! hs'
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl :
  Membership.mem (γ := Set ↥L.lattice)
    {x : ↥L.lattice |
        (fun (n : ↥L.lattice) ↦ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n) x}ᶜ
    l
s : ℂ
hs : ‖s‖ < r
hs' : R < ‖l‖
⊢ ‖f l s‖ ≤ u r l

Tactic:
hR _ hs'.le _ hs _ rfl

Premises used: LT.lt.le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ b ≥ R, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl :
  Membership.mem (γ := Set ↥L.lattice)
    {x : ↥L.lattice |
        (fun (n : ↥L.lattice) ↦ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n) x}ᶜ
    l
s : ℂ
hs : ‖s‖ < r
hs' : R < ‖l‖
⊢ ‖f l s‖ ≤ u r l

Tactic:
exact hR _ hs'.le _ hs _ rfl

Premises used: LT.lt.le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖s‖
linarith : 0 - r + (‖s‖ - r) + (2 * r - ‖s‖) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
⊢ s ≠ l

Tactic:
have : s ≠ ↑l := by rintro rfl; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this : s ≠ l
linarith : ‖l‖ ≤ 0 → 2 * (0 - r) + (2 * r - ‖l‖) + (‖l‖ - 0) = 0
linarith₁ : ‖l‖ ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < ‖l‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this : s ≠ l
⊢ 0 < ‖l‖

Tactic:
have : 0 < ‖l‖ := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
hb : HPow.hPow (β := ℕ) (s - l) 2 ≠ 0
hd : HPow.hPow (β := ℕ) l 2 ≠ 0
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖

Tactic:
rw [div_sub_div, one_mul, mul_one]

Premises used: mul_one, div_sub_div, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ HPow.hPow (β := ℕ) (s - l) 2 ≠ 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ HPow.hPow (β := ℕ) l 2 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
hdb : ‖l‖ / 2 ≤ ‖s - l‖
⊢ ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
hdb : ‖l‖ / 2 ≤ ‖l - s‖
⊢ ‖l‖ / 2 ≤ ‖s - l‖

Tactic:
rw [norm_sub_rev]

Premises used: norm_sub_rev
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
linarith : ‖l‖ - ‖s‖ < ‖l‖ / 2 → 2 / 2 = 1
linarith₁ : ‖l‖ - ‖s‖ < ‖l‖ / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ‖l‖ - ‖s‖ < ‖l‖ / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : ‖l‖ - ‖s‖ < ‖l‖ / 2 → 2 * (‖s‖ - r) + (2 * r - ‖l‖) + (2 * ‖l‖ - 2 * ‖s‖ - 1 * ‖l‖) = 0
linarith₄ : ‖l‖ - ‖s‖ < ‖l‖ / 2 → GT.gt (α := ℝ) 2 0
⊢ ‖l‖ / 2 ≤ ‖l‖ - ‖s‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖l - s‖

Tactic:
exact .trans (by linarith) (norm_sub_norm_le l s)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
e_a : ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ = ‖s * (2 * l - s)‖
e_a₁ : HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2 = HPow.hPow (β := ℕ) ‖l‖ 4 / 4
⊢ ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
e_a : ‖(l + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖
⊢ ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ = ‖s * (2 * l - s)‖

Tactic:
rw [sq_sub_sq]

Premises used: sq_sub_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖

Tactic:
simp [← sub_add, two_mul, sub_add_eq_add_sub]

Premises used: sub_add, two_mul, sub_add_eq_add_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2 = HPow.hPow (β := ℕ) ‖l‖ 4 / 4

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
hab : ‖2 * l - s‖ ≤ 2.5 * ‖l‖
⊢ 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4 ≤ 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4

Tactic:
gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4

Premises used: HMul.hMul, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ ‖2 * l - s‖ ≤ 2.5 * ‖l‖

Tactic:
(norm_sub_le _ _).trans ?_

Premises used: norm_sub_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
hab : ‖2 * l‖ + ‖s‖ ≤ 2.5 * ‖l‖
⊢ ‖2 * l - s‖ ≤ 2.5 * ‖l‖

Tactic:
refine (norm_sub_le _ _).trans ?_

Premises used: norm_sub_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
hab : 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖
⊢ ‖2 * l‖ + ‖s‖ ≤ 2.5 * ‖l‖

Tactic:
simp only [Complex.norm_mul, Complex.norm_ofNat]

Premises used: Complex.norm_ofNat, Complex.norm_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
linarith : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → 2 / 2 = 1
linarith₁ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → GT.gt (α := ℝ) 2 0
linarith₅ :
  2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ →
    2 * (‖s‖ - r) + (2 * r - ‖l‖) +
        (HMul.hMul (α := ℝ) 1 5 * (1 * ‖l‖) - (HMul.hMul (α := ℝ) 1 2 * (2 * ‖l‖) + 2 * ‖s‖)) =
      0
linarith₆ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → GT.gt (α := ℝ) 2 0
⊢ 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4 = 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3 = 10 * r * ‖l‖ ^ Int.negSucc 2
⊢ 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3 = 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
_ :
  ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ =
    ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖
_₁ :
  ‖(HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2) / (HPow.hPow (β := ℕ) (s - l) 2 * HPow.hPow (β := ℕ) l 2)‖ =
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₂ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ / (HPow.hPow (β := ℕ) ‖s - l‖ 2 * HPow.hPow (β := ℕ) ‖l‖ 2) ≤
    ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
_₃ :
  ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ /
      (HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₄ : ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
_₅ : ‖s‖ * ‖2 * l - s‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4) = 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4
_₆ : 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4 ≤ 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4
_₇ : 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4 = 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3
_₈ : 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3 = 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)

Tactic:
calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast

Premises used: Norm.norm, HMul.hMul, HSub.hSub, HDiv.hDiv, OfScientific.ofScientific, Bool.true, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
x : ℝ
h : x > 0
simp : LT.lt (α := ℝ) 2 3
⊢ LT.lt (α := ℝ) (-3) (-(↑(finrank ℤ ↥L.lattice) : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
x : ℝ
h : x > 0
⊢ LT.lt (α := ℝ) 2 3

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
refine :
  ∀ (r : ℝ) (hr : r > 0),
    ∀ b ≥ 2 * r,
      ∀ (x : ℂ),
        ‖x‖ < r →
          ∀ (l : ↥L.lattice),
            ‖(↑l : ℂ)‖ = b →
              ‖if (↑l : ℂ) = l₀ then 0
                  else 1 / HPow.hPow (β := ℕ) (x - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2‖ ≤
                (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l
⊢ HasSumLocallyUniformly
    (fun (l : ↥L.lattice) (z : ℂ) ↦
      if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    ℘[L - l₀]

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

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

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : (↑l : ℂ) = l₀
⊢ 0 ≤ 10 * r * (HPow.hPow (β := ℕ) ‖l‖ 3)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : (↑l : ℂ) = l₀
⊢ norm (E := ℂ) 0 ≤ (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l

Tactic:
simpa using show 0 ≤ 10 * r * (‖↑l‖ ^ 3)⁻¹ by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
⊢ ‖1 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2‖ ≤
    (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l

Tactic:
weierstrassP_bound r hr s hs l h

Premises used: PeriodPair.weierstrassP_bound, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
⊢ ‖1 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2‖ ≤
    (fun (x1 : ℝ) (x2 : ↥L.lattice) ↦ 10 * x1 * HPow.hPow (β := ℝ) ‖x2‖ (-3)) r l

Tactic:
exact weierstrassP_bound r hr s hs l h

Premises used: PeriodPair.weierstrassP_bound, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
⊢ HasSum
    (fun (l : ↥L.lattice) ↦
      if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
    (℘[L - l₀] z)

Tactic:
(L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSum

Premises used: HasSumLocallyUniformly.hasSum, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ DifferentiableOn ℂ ℘[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
(L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSumLocallyUniformlyOn.differentiableOn
    (.of_forall fun s ↦ .fun_sum fun i hi ↦ ?_) L.isOpen_compl_lattice_diff

Premises used: Filter.Eventually.of_forall, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, DifferentiableOn.fun_sum, PeriodPair.isOpen_compl_lattice_diff, TendstoLocallyUniformlyOn.differentiableOn, HasSumLocallyUniformly.hasSumLocallyUniformlyOn
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
refine :
  ∀ (s : Finset ↥L.lattice) (i : ↥L.lattice) (hi : i ∈ s),
    DifferentiableOn ℂ (F := ℂ)
      (fun (z : ℂ) ↦
        if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
      ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ DifferentiableOn ℂ ℘[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
refine (L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSumLocallyUniformlyOn.differentiableOn
    (.of_forall fun s ↦ .fun_sum fun i hi ↦ ?_) L.isOpen_compl_lattice_diff

Premises used: Filter.Eventually.of_forall, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, DifferentiableOn.fun_sum, PeriodPair.isOpen_compl_lattice_diff, TendstoLocallyUniformlyOn.differentiableOn, HasSumLocallyUniformly.hasSumLocallyUniformlyOn