awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
⊢ DifferentiableOn ℂ ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have 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₀})ᶜ
Tactic: refine L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀
    |>.tendstoLocallyUniformlyOn.differentiableOn
      (.of_forall fun s ↦ .fun_sum fun i hi ↦ ?_) L.isOpen_compl_lattice_diff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
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₀})ᶜ
have pos : (↑i : ℂ) = l₀ → DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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₀})ᶜ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ if (↑i : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have neg : ¬(↑i : ℂ) = l₀ →
  DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -2 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -2 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 3) ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have neg : ∀ (x : ℂ) (hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ), HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 3 ≠ 0
Tactic: refine .div (by fun_prop) (by fun_prop) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 3 ≠ 0
have this : x ≠ (↑i : ℂ)
Tactic: have : x ≠ i := by rintro rfl; simp_all
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
⊢ Set.EqOn (deriv ℘[L - l₀]) ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have 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₀})ᶜ
Tactic: refine ((L.hasSumLocallyUniformly_weierstrassPExcept l₀).tendstoLocallyUniformlyOn.deriv
    (.of_forall fun s ↦ ?_) L.isOpen_compl_lattice_diff).unique ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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₀})ᶜ
⊢ Set.EqOn (deriv ℘[L - l₀]) ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have 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₀})ᶜ
Tactic: refine ((L.hasSumLocallyUniformly_weierstrassPExcept l₀).tendstoLocallyUniformlyOn.deriv
    (.of_forall fun s ↦ ?_) L.isOpen_compl_lattice_diff).unique ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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₀})ᶜ
have 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₀})ᶜ
Tactic: refine .fun_sum fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - (↑i : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑i : ℂ) 2)
    ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have neg : ∀ (x : ℂ) (hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ), HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 2 ≠ 0
Tactic: refine .sub (.div (by fun_prop) (by fun_prop) fun x hx ↦ ?_) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h : ¬(↑i : ℂ) = l₀
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ HPow.hPow (β := ℕ) (x - (↑i : ℂ)) 2 ≠ 0
have this : x ≠ (↑i : ℂ)
Tactic: have : x ≠ i := by rintro rfl; simp_all
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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₀})ᶜ
have 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₀})ᶜ
Tactic: refine (L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.congr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {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)
have 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)
Tactic: rw [deriv_fun_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
⊢ 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)
have 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
Tactic: rw [deriv_fun_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {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)
have 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
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
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
have pos : ∀ (hl₁ : (↑x : ℂ) = l₀), Eq (α := ℂ) 0 (deriv (fun (x2 : ℂ) ↦ 0) l)
Tactic: split_ifs with hl₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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)
⊢ (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
have 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
Tactic: split_ifs with hl₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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₀
have hl₂ : (↑x : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: obtain rfl := sub_eq_zero.mp e
Cleared hypotheses: l, hl, e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
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 : ℂ) = l₀
have e₁ : (↑x : ℂ) - (↑x : ℂ) = 0
Tactic: obtain rfl := sub_eq_zero.mp e
Cleared hypotheses: l, hl, e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hl₁ : ¬(↑x : ℂ) = l₀
⊢ -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
    deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l
have hl₂ : l - (↑x : ℂ) ≠ 0
Tactic: have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
    deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l
have neg : -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
  HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2) l) 0
Tactic: rw [deriv_fun_sub (.fun_div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop),
        deriv_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
    HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2) l) 0
have neg : -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 =
  HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ HPow.hPow (β := ℤ) (x2 - (↑x : ℂ)) (-2)) l) 0
Tactic: simp_rw [← zpow_natCast, one_div, ← zpow_neg, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 =
    HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ HPow.hPow (β := ℤ) (x2 - (↑x : ℂ)) (-2)) l) 0
have neg : -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 = (↑(-2) : ℂ) * (l - (↑x : ℂ)) ^ HSub.hSub (α := ℤ) (-2) 1 - 0
Tactic: rw [deriv_comp_sub_const (f := (· ^ (-2 : ℤ))), deriv_zpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
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
⊢ -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 = (↑(-2) : ℂ) * (l - (↑x : ℂ)) ^ HSub.hSub (α := ℤ) (-2) 1 - 0
have neg : -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 = -(2 * (HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3)⁻¹)
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x2 : ℂ) ↦
      if (↑x : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2)
    l
have pos : ∀ (hl₁ : (↑x : ℂ) = l₀), DifferentiableAt ℂ (F := ℂ) (fun (x2 : ℂ) ↦ 0) l
Tactic: split_ifs with hl₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
pos : ∀ (hl₁ : (↑x : ℂ) = l₀), DifferentiableAt ℂ (F := ℂ) (fun (x2 : ℂ) ↦ 0) l
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x2 : ℂ) ↦
      if (↑x : ℂ) = l₀ then 0 else 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2)
    l
have neg : ∀ (hl₁ : ¬(↑x : ℂ) = l₀),
  DifferentiableAt ℂ (F := ℂ)
    (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l
Tactic: split_ifs with hl₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁ : ¬(↑x : ℂ) = l₀
e : l - (↑x : ℂ) = 0
⊢ (↑x : ℂ) = l₀
have hl₂ : (↑x : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: obtain rfl := sub_eq_zero.mp e
Cleared hypotheses: l, hl, e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁ : ¬(↑x : ℂ) = l₀
e : l - (↑x : ℂ) = 0
hl₂ : (↑x : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ (↑x : ℂ) = l₀
have e₁ : (↑x : ℂ) - (↑x : ℂ) = 0
Tactic: obtain rfl := sub_eq_zero.mp e
Cleared hypotheses: l, hl, e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁ : ¬(↑x : ℂ) = l₀
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l
have hl₂ : l - (↑x : ℂ) ≠ 0
Tactic: have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
⊢ Eq (α := ℂ) (∑' (l : ↥L.lattice), if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (-z - (↑l : ℂ)) 3)
    (-∑' (l : ↥L.lattice), if (↑l : ℂ) = -l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
have rw : Eq (α := ℂ)
  (∑' (c : ↥L.lattice),
    if (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
    else -2 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
  (-∑' (l : ↥L.lattice), if (↑l : ℂ) = -l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
Tactic: rw [← (Equiv.neg L.lattice).tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
⊢ Eq (α := ℂ)
    (∑' (c : ↥L.lattice),
      if (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
      else -2 / HPow.hPow (β := ℕ) (-z - (↑((Equiv.neg ↥L.lattice : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
    (-∑' (l : ↥L.lattice), if (↑l : ℂ) = -l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
have simp : Eq (α := ℂ) (∑' (c : ↥L.lattice), if -(↑c : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) ((↑c : ℂ) - z) 3)
  (∑' (b : ↥L.lattice), if (↑b : ℂ) = -l₀ then 0 else -2 / -HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
Tactic: simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub,
    ← div_neg, ← tsum_neg, apply_ite, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
⊢ Eq (α := ℂ) (∑' (c : ↥L.lattice), if -(↑c : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) ((↑c : ℂ) - z) 3)
    (∑' (b : ↥L.lattice), if (↑b : ℂ) = -l₀ then 0 else -2 / -HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
have h : ∀ (l : ↥L.lattice), -(↑l : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀
Tactic: congr! 3 with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
h : ∀ (l : ↥L.lattice), -(↑l : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀
⊢ Eq (α := ℂ) (∑' (c : ↥L.lattice), if -(↑c : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) ((↑c : ℂ) - z) 3)
    (∑' (b : ↥L.lattice), if (↑b : ℂ) = -l₀ then 0 else -2 / -HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
have h₁ : ∀ (l : ↥L.lattice),
  ¬(↑l : ℂ) = -l₀ → -2 / HPow.hPow (β := ℕ) ((↑l : ℂ) - z) 3 = -2 / -HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
Tactic: congr! 3 with l
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ Eq (α := ℂ)
    (∑' (l_1 : ↥L.lattice), if (↑l_1 : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l_1 : ℂ)) 3)
    (∑' (l_1 : ↥L.lattice), if (↑l_1 : ℂ) = l₀ - (↑l : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l_1 : ℂ)) 3)
have rw : Eq (α := ℂ)
  (∑' (c : ↥L.lattice),
    if (↑((Equiv.addRight l : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ) = l₀ then 0
    else -2 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑((Equiv.addRight l : (a : ↥L.lattice) → ↥L.lattice) c) : ℂ)) 3)
  (∑' (l_1 : ↥L.lattice), if (↑l_1 : ℂ) = l₀ - (↑l : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l_1 : ℂ)) 3)
Tactic: rw [← (Equiv.addRight l).tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ)))
    (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
have apply : IsPreconnected ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
Tactic: apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_diff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
apply : IsPreconnected ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
⊢ Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ)))
    (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
have apply₁ : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ))) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
Tactic: apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_diff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
apply : IsPreconnected ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
apply₁ : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ))) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
⊢ Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ)))
    (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
have apply₂ : DifferentiableOn ℂ (F := ℂ)
  (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
  ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
Tactic: apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_diff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
apply : IsPreconnected ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
apply₁ : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ))) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
apply₂ :
  DifferentiableOn ℂ (F := ℂ)
    (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
⊢ Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ)))
    (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
have apply₃ : Set.EqOn (β := ℂ) (deriv fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ)))
  (deriv fun (x : ℂ) ↦
    ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
  ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
Tactic: apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_diff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
apply : IsPreconnected ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
apply₁ : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ))) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
apply₂ :
  DifferentiableOn ℂ (F := ℂ)
    (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
apply₃ :
  Set.EqOn (β := ℂ) (deriv fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ)))
    (deriv fun (x : ℂ) ↦
      ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
⊢ Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ)))
    (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
have apply₄ : -((↑l : ℂ) / 2) ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
Tactic: apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_diff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_