awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≤ 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 (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l

Tactic:
simpa using show 0 ≤ ‖↑l‖ ^ 3 by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
l : ↥L.lattice
h : ‖(↑l : ℂ)‖ ≥ 2 * r
h_1 : ¬(↑l : ℂ) = l₀
hs : ‖(↑l : ℂ)‖ < r
linarith : 0 - r + (2 * r - ‖(↑l : ℂ)‖) + (‖(↑l : ℂ)‖ - r) = 0
⊢ False

Tactic:
linarith
-- 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₀
⊢ s ≠ (↑l : ℂ)

Tactic:
have : s ≠ ↑l := by rintro rfl; exfalso; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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 : ℂ)
⊢ 0 < r

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
⊢ ‖s‖ < r

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
⊢ 2 * r ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
⊢ ¬0 = l₀

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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₀
⊢ ¬s = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
linarith₁ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith
-- 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₀
this : s ≠ (↑l : ℂ)
⊢ l ≠ 0

Tactic:
have : l ≠ 0 := by rintro rfl; simp_all; linarith
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : 2 / HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3 ≤ 16 * HPow.hPow (β := ℝ) ‖l‖ (-3)
⊢ ‖-2 / HPow.hPow (β := ℕ) (s - (↑l : ℂ)) 3‖ ≤ (fun (x : ℝ) (x_1 : ↥L.lattice) ↦ 16 * HPow.hPow (β := ℝ) ‖x_1‖ (-3)) r l

Tactic:
simp only [Complex.norm_div, norm_neg, Complex.norm_ofNat, norm_pow]

Premises used: norm_pow, Complex.norm_div, Complex.norm_ofNat, norm_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
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 0 ≤ ‖l‖

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₀
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
neg₂ : 0 < HPow.hPow (β := ℝ) ‖l‖ 3
⊢ 2 / HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3 ≤ 16 * HPow.hPow (β := ℝ) ‖l‖ (-3)

Tactic:
rw [Real.rpow_neg (by positivity), ← div_eq_mul_inv, div_le_div_iff₀, norm_sub_rev]

Premises used: div_eq_mul_inv, div_le_div_iff₀, norm_sub_rev, Real.rpow_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
h_1 : ¬(↑l : ℂ) = l₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3 = 16 * HPow.hPow (β := ℕ) ‖(↑l : ℂ) - s‖ 3

Tactic:
ring
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3
⊢ 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 16 * HPow.hPow (β := ℕ) ‖(↑l : ℂ) - s‖ 3

Tactic:
refine LE.le.trans_eq (b := 2 * (2 * ‖l - s‖) ^ 3) ?_ (by ring)

Premises used: LE.le.trans_eq
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : 2 * HPow.hPow (β := ℕ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3
⊢ 2 * HPow.hPow (β := ℝ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3

Tactic:
norm_cast
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : ‖l‖ ≤ 2 * ‖(↑l : ℂ) - s‖
⊢ 2 * HPow.hPow (β := ℕ) ‖l‖ 3 ≤ 2 * HPow.hPow (β := ℕ) (2 * ‖(↑l : ℂ) - s‖) 3

Tactic:
gcongr
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
linarith : ‖(↑l : ℂ)‖ - ‖s‖ < 0 → 0 - r + (‖s‖ - r) + (2 * r - ‖(↑l : ℂ)‖) + (‖(↑l : ℂ)‖ - ‖s‖ - 0) = 0
⊢ 0 ≤ ‖(↑l : ℂ)‖ - ‖s‖

Tactic:
linarith
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
linarith₁ : LT.lt (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
⊢ LE.le (α := ℝ) 0 2

Tactic:
linarith
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : ‖l‖ ≤ 2 * (‖(↑l : ℂ)‖ - ‖s‖)
⊢ ‖l‖ ≤ 2 * ‖(↑l : ℂ) - s‖

Tactic:
refine le_trans ?_ (mul_le_mul le_rfl (norm_sub_norm_le _ _) (by linarith) (by linarith))

Premises used: le_rfl, mul_le_mul, norm_sub_norm_le, le_trans
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
neg : ∀ (hr : r > 0), ‖l‖ ≤ 2 * (‖l‖ - ‖s‖)
⊢ ‖l‖ ≤ 2 * (‖(↑l : ℂ)‖ - ‖s‖)

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
linarith₁ : 2 * (‖l‖ - ‖s‖) < ‖l‖ → GT.gt (α := ℝ) 2 0
⊢ ‖l‖ ≤ 2 * (‖l‖ - ‖s‖)

Tactic:
linarith
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 0 < ‖s - (↑l : ℂ)‖

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) ‖s - (↑l : ℂ)‖ 3

Tactic:
exact pow_pos (by simpa [sub_eq_zero]) _

Premises used: pow_pos
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 0 < ‖l‖

Tactic:
simpa
-- 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₀
this_1 : s ≠ (↑l : ℂ)
this : l ≠ 0
⊢ 0 < HPow.hPow (β := ℝ) ‖l‖ 3

Tactic:
exact Real.rpow_pos_of_pos (by simpa) _

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

Tactic:
(L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.tendsto_at
    (Set.mem_univ z)

Premises used: iInf, TendstoLocallyUniformly.tendstoLocallyUniformlyOn, Filter.atTop, TendstoLocallyUniformlyOn.tendsto_at, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, HasSum, Set.mem_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ DifferentiableOn ℂ ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀
    |>.tendstoLocallyUniformlyOn.differentiableOn
      (.of_forall fun s ↦ .fun_sum fun i hi ↦ ?_) L.isOpen_compl_lattice_diff

Premises used: TendstoLocallyUniformly.tendstoLocallyUniformlyOn, Filter.Eventually.of_forall, DifferentiableOn.fun_sum, PeriodPair.isOpen_compl_lattice_diff, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, TendstoLocallyUniformlyOn.differentiableOn
-- 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 -2 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3)
      ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ DifferentiableOn ℂ ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
refine L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀
    |>.tendstoLocallyUniformlyOn.differentiableOn
      (.of_forall fun s ↦ .fun_sum fun i hi ↦ ?_) L.isOpen_compl_lattice_diff

Premises used: TendstoLocallyUniformly.tendstoLocallyUniformlyOn, Filter.Eventually.of_forall, DifferentiableOn.fun_sum, PeriodPair.isOpen_compl_lattice_diff, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, TendstoLocallyUniformlyOn.differentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
pos : (↑i : ℂ) = l₀ → DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
neg :
  ¬(↑i : ℂ) = l₀ →
    DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -2 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ if (↑i : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -2) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
neg : ∀ (x : ℂ) (hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ), HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 3 ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -2 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
refine .div (by fun_prop) (by fun_prop) fun x hx ↦ ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
hx : (↑i : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ x ≠ (↑i : ℂ)

Tactic:
have : x ≠ i := by rintro rfl; simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
this : x ≠ (↑i : ℂ)
⊢ HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 3 ≠ 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ Set.EqOn (deriv ℘[L - l₀]) ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
((L.hasSumLocallyUniformly_weierstrassPExcept l₀).tendstoLocallyUniformlyOn.deriv
    (.of_forall fun s ↦ ?_) L.isOpen_compl_lattice_diff).unique ?_

Premises used: TendstoLocallyUniformlyOn.unique, TendstoLocallyUniformly.tendstoLocallyUniformlyOn, Filter.Eventually.of_forall, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, TendstoLocallyUniformlyOn.deriv, PeriodPair.isOpen_compl_lattice_diff
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
refine_1 :
  ∀ (s : Finset ↥L.lattice),
    DifferentiableOn ℂ (F := ℂ)
      (fun (x2 : ℂ) ↦
        ∑ i ∈ s,
          (fun (l : ↥L.lattice) (z : ℂ) ↦
              if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
            i x2)
      ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
refine_2 :
  TendstoLocallyUniformlyOn (ι := Finset ↥L.lattice)
    (deriv ∘ fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦
      ∑ i ∈ x1,
        (fun (l : ↥L.lattice) (z : ℂ) ↦
            if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
          i x2)
    ℘'[L - l₀] atTop ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ Set.EqOn (deriv ℘[L - l₀]) ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
refine ((L.hasSumLocallyUniformly_weierstrassPExcept l₀).tendstoLocallyUniformlyOn.deriv
    (.of_forall fun s ↦ ?_) L.isOpen_compl_lattice_diff).unique ?_

Premises used: TendstoLocallyUniformlyOn.unique, TendstoLocallyUniformly.tendstoLocallyUniformlyOn, Filter.Eventually.of_forall, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, TendstoLocallyUniformlyOn.deriv, PeriodPair.isOpen_compl_lattice_diff
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (x2 : ℂ) ↦
      ∑ i ∈ s,
        (fun (l : ↥L.lattice) (z : ℂ) ↦
            if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
          i x2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
.fun_sum fun i hi ↦ ?_

Premises used: DifferentiableOn.fun_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
refine_1 :
  ∀ (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 ℂ (F := ℂ)
    (fun (x2 : ℂ) ↦
      ∑ i ∈ s,
        (fun (l : ↥L.lattice) (z : ℂ) ↦
            if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
          i x2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
refine .fun_sum fun i hi ↦ ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
neg : ∀ (x : ℂ) (hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ), HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 2 ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
refine .sub (.div (by fun_prop) (by fun_prop) fun x hx ↦ ?_) (by fun_prop)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
this : x ≠ (↑i : ℂ)
⊢ HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 2 ≠ 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ TendstoLocallyUniformlyOn (ι := Finset ↥L.lattice)
    (deriv ∘ fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦
      ∑ i ∈ x1,
        (fun (l : ↥L.lattice) (z : ℂ) ↦
            if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
          i x2)
    ℘'[L - l₀] atTop ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
(L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.congr ?_

Premises used: TendstoLocallyUniformly.tendstoLocallyUniformlyOn, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, TendstoLocallyUniformlyOn.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
refine_2 :
  ∀ (n : Finset ↥L.lattice),
    Set.EqOn (β := ℂ)
      (fun (x2 : ℂ) ↦
        ∑ i ∈ n,
          (fun (l : ↥L.lattice) (z : ℂ) ↦ if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) i x2)
      ((deriv ∘ fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦
          ∑ i ∈ x1,
            (fun (l : ↥L.lattice) (z : ℂ) ↦
                if (↑l : ℂ) = l₀ then 0
                else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
              i x2)
        n)
      ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ TendstoLocallyUniformlyOn (ι := Finset ↥L.lattice)
    (deriv ∘ fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦
      ∑ i ∈ x1,
        (fun (l : ↥L.lattice) (z : ℂ) ↦
            if (↑l : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑l : ℂ) 2)
          i x2)
    ℘'[L - l₀] atTop ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
refine (L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.congr ?_

Premises used: TendstoLocallyUniformly.tendstoLocallyUniformlyOn, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, TendstoLocallyUniformlyOn.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
refine_2 :
  Eq (α := ℂ) (∑ x ∈ s, if (↑x : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3)
    (∑ i ∈ s,
      deriv
        (fun (x2 : ℂ) ↦
          if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
        l)
refine_2₁ :
  ∀ i ∈ s,
    DifferentiableAt ℂ (F := ℂ)
      (fun (x2 : ℂ) ↦
        if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
      l
⊢ Eq (α := ℂ) (∑ x ∈ s, if (↑x : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3)
    (deriv
      (fun (x2 : ℂ) ↦
        ∑ x ∈ s,
          if (↑x : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2)
      l)

Tactic:
rw [deriv_fun_sum]

Premises used: deriv_fun_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
refine_2 :
  ∀ (x : ↥L.lattice),
    (if (↑x : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3) =
      deriv
        (fun (x2 : ℂ) ↦
          if (↑x : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2)
        l
⊢ Eq (α := ℂ) (∑ x ∈ s, if (↑x : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3)
    (∑ i ∈ s,
      deriv
        (fun (x2 : ℂ) ↦
          if (↑i : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
        l)

Tactic:
congr with x
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
pos : ∀ (hl₁ : (↑x : ℂ) = l₀), Eq (α := ℂ) 0 (deriv (fun (x2 : ℂ) ↦ 0) l)
neg :
  ∀ (hl₁ : ¬(↑x : ℂ) = l₀),
    -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
      deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l
⊢ (if (↑x : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3) =
    deriv
      (fun (x2 : ℂ) ↦
        if (↑x : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2)
      l

Tactic:
split_ifs with hl₁
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁ : (↑x : ℂ) = l₀
⊢ Eq (α := ℂ) 0 (deriv (fun (x2 : ℂ) ↦ 0) l)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁ : ¬(↑x : ℂ) = l₀
e : l - (↑x : ℂ) = 0
⊢ (↑x : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
obtain rfl := sub_eq_zero.mp e

Premises used: sub_eq_zero, Iff.mp, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁ : ¬(↑x : ℂ) = l₀
e : l - (↑x : ℂ) = 0
hl₂ : (↑x : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ (↑x : ℂ) - (↑x : ℂ) = 0

Tactic:
obtain rfl := sub_eq_zero.mp e

Premises used: sub_eq_zero, Iff.mp, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
x : ↥L.lattice
hl₁ : ¬(↑x : ℂ) = l₀
hl : (↑x : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
e : (↑x : ℂ) - (↑x : ℂ) = 0
⊢ (↑x : ℂ) = l₀

Tactic:
simpa using hl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁ : ¬(↑x : ℂ) = l₀
⊢ l - (↑x : ℂ) ≠ 0

Tactic:
have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ 1) l

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x_1 : ℂ) ↦ HPow.hPow (β := ℕ) (x_1 - (↑x : ℂ)) 2) l

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 2 ≠ 0

Tactic:
simpa