awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
α β : ℤ
h : Rat.den (↑α : ℚ) = 1 ∧ Rat.den (↑β : ℚ) = 1
⊢ (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑(↑β : ℚ) : ℂ) * L.ω₂ ∈ L.lattice
have refine_2 : α • L.ω₁ + β • L.ω₂ ∈ L.lattice
Tactic: simp only [Rat.cast_intCast, ← zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
⊢ L.lattice = Submodule.span ℤ (Set.range (ι := Fin 2) (⇑L.basis : (a : Fin 2) → ℂ))
have this : Eq (α := Finset (Fin 2)) Finset.univ {0, 1}
Tactic: have : Finset.univ (α := Fin 2) = {0, 1} := rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
this : Eq (α := Finset (Fin 2)) Finset.univ {0, 1}
⊢ L.lattice = Submodule.span ℤ (Set.range (ι := Fin 2) (⇑L.basis : (a : Fin 2) → ℂ))
have rw : Eq (α := Submodule ℤ ℂ) (Submodule.span ℤ {L.ω₁, L.ω₂})
  (Submodule.span ℤ ((⇑L.basis : (a : Fin 2) → ℂ) '' (↑{0, 1} : Set (Fin 2))))
Tactic: rw [lattice, ← Set.image_univ, ← Finset.coe_univ, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
L : PeriodPair
⊢ IsZLattice ℝ L.lattice
have simp_rw : IsZLattice ℝ (E := ℂ) (Submodule.span ℤ (Set.range (ι := Fin 2) (⇑L.basis : (a : Fin 2) → ℂ)))
Tactic: simp_rw [L.lattice_eq_span_range_basis]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
s : Set ℂ
hs : s ⊆ (↑L.lattice : Set ℂ)
⊢ IsClosed s
have h : s =
  Set.image (α := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
    (Subtype.val (p := fun (x : ℂ) ↦ x ∈ L.lattice) ⁻¹' s)
Tactic: convert!
    L.isClosed_lattice.isClosedMap_subtype_val _ (isClosed_discrete (α := L.lattice) ((↑) ⁻¹' s))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
s : Set ℂ
hs : s ⊆ (↑L.lattice : Set ℂ)
⊢ s =
    Set.image (α := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
      (Subtype.val (p := fun (x : ℂ) ↦ x ∈ L.lattice) ⁻¹' s)
have h : s =
  s ∩ Set.range (ι := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
Tactic: convert! Set.image_preimage_eq_inter_range.symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ HasSumLocallyUniformly f fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x
have rw : ∀ (x : ℂ),
  TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)
Tactic: rw [hasSumLocallyUniformly_iff_tendstoLocallyUniformly, tendstoLocallyUniformly_iff_filter]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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 : ℂ
⊢ TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)
have obtain : ∀ (r : ℝ) (hr : 0 < r) (hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)),
  TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)
Tactic: obtain ⟨r, hr, hr'⟩ : ∃ r, 0 < r ∧ 𝓝 x ≤ 𝓟 (Metric.ball 0 r) :=
    ⟨‖x‖ + 1, by positivity, Filter.le_principal_iff.mpr (Metric.isOpen_ball.mem_nhds (by simp))⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
⊢ TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)
have refine : TendstoUniformlyOnFilter (β := ℂ) (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 .mono_right ?_ hr'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
⊢ TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓟 (Metric.ball 0 r))
have rw : 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: rw [← tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
⊢ 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)
have refine : ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n
Tactic: refine tendstoUniformlyOn_tsum_of_cofinite_eventually (hu r hr) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
⊢ ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (Metric.ball 0 r) x → ‖f n x‖ ≤ u r n
have 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
Tactic: obtain ⟨R, hR⟩ := eventually_atTop.mp (hf r hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
have 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)
Tactic: refine (isCompact_iff_finite.mp (isCompact_closedBall (0 : L.lattice) R)).subset ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ Membership.mem (γ := Set ↥L.lattice) (Metric.closedBall 0 R) l
have obtain : ∀ (s : ℂ) (hs : ‖s‖ < r) (hs' : u r l < ‖f l s‖), 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖
⊢ Membership.mem (γ := Set ↥L.lattice) (Metric.closedBall 0 R) l
have simp : ‖l‖ ≤ R
Tactic: simp only [Metric.mem_closedBall, dist_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖
⊢ ‖l‖ ≤ R
have contrapose! : ∀ (hs' : R < ‖l‖), ‖f l s‖ ≤ u r l
Tactic: contrapose! hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖s‖
⊢ False
have linarith : 0 - r + (‖s‖ - r) + (2 * r - ‖s‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have this : s ≠ l
Tactic: have : s ≠ ↑l := by rintro rfl; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this : s ≠ l
⊢ 0 < ‖l‖
have linarith : ‖l‖ ≤ 0 → 2 * (0 - r) + (2 * r - ‖l‖) + (‖l‖ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ 0 < ‖l‖
have linarith₁ : ‖l‖ ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this : s ≠ l
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have this₁ : 0 < ‖l‖
Tactic: have : 0 < ‖l‖ := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)‖
have hb : HPow.hPow (β := ℕ) (s - l) 2 ≠ 0
Tactic: rw [div_sub_div, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ‖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)‖
have hd : HPow.hPow (β := ℕ) l 2 ≠ 0
Tactic: rw [div_sub_div, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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 (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2)
have hdb : ‖l‖ / 2 ≤ ‖s - l‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖s - l‖
have hdb : ‖l‖ / 2 ≤ ‖l - s‖
Tactic: rw [norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖
have linarith : ‖l‖ - ‖s‖ < ‖l‖ / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ‖l‖ / 2 ≤ ‖l‖ - ‖s‖
have linarith₁ : ‖l‖ - ‖s‖ < ‖l‖ / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ‖l‖ / 2 ≤ ‖l‖ - ‖s‖
have linarith₂ : ‖l‖ - ‖s‖ < ‖l‖ / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ ‖l‖ / 2 ≤ ‖l‖ - ‖s‖
have linarith₃ : ‖l‖ - ‖s‖ < ‖l‖ / 2 → 2 * (‖s‖ - r) + (2 * r - ‖l‖) + (2 * ‖l‖ - 2 * ‖s‖ - 1 * ‖l‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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 (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2) =
    ‖s * (2 * l - s)‖ / (HPow.hPow (β := ℕ) ‖l‖ 4 / 4)
have e_a : ‖HPow.hPow (β := ℕ) l 2 - HPow.hPow (β := ℕ) (s - l) 2‖ = ‖s * (2 * l - s)‖
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)‖
⊢ ‖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)
have e_a₁ : HPow.hPow (β := ℕ) (‖l‖ / 2) 2 * HPow.hPow (β := ℕ) ‖l‖ 2 = HPow.hPow (β := ℕ) ‖l‖ 4 / 4
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖ = ‖s * (2 * l - s)‖
have e_a : ‖(l + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖
Tactic: rw [sq_sub_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ 4 * ‖s‖ * ‖2 * l - s‖ / HPow.hPow (β := ℕ) ‖l‖ 4 ≤ 4 * r * (2.5 * ‖l‖) / HPow.hPow (β := ℕ) ‖l‖ 4
have hab : ‖2 * l - s‖ ≤ 2.5 * ‖l‖
Tactic: gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖
have hab : ‖2 * l‖ + ‖s‖ ≤ 2.5 * ‖l‖
Tactic: refine (norm_sub_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖
have hab : 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖
Tactic: simp only [Complex.norm_mul, Complex.norm_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖
have linarith : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖
have linarith₁ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖
have linarith₂ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖
have linarith₄ : 2.5 * ‖l‖ < 2 * ‖l‖ + ‖s‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this_1 : s ≠ l
this : 0 < ‖l‖
⊢ 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3 = 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have norm_cast : 10 * r / HPow.hPow (β := ℕ) ‖l‖ 3 = 10 * r * ‖l‖ ^ Int.negSucc 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _ : ‖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: 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)‖
⊢ ‖1 / HPow.hPow (β := ℕ) (s - l) 2 - 1 / HPow.hPow (β := ℕ) l 2‖ ≤ 10 * r * HPow.hPow (β := ℝ) ‖l‖ (-3)
have _₁ : ‖(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: 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