awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ)})ᶜ
apply₄ : -((↑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 - l₀] (-((↑l : ℂ) / 2) + (↑l : ℂ)) =
  ℘[L - l₀ - (↑l : ℂ)] (-((↑l : ℂ) / 2)) + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2)
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
⊢ IsPreconnected ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
have refine : ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)}).Countable
Tactic: refine (Set.Countable.isConnected_compl_of_one_lt_rank (by simp) ?_).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
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ))) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
have refine : Set.MapsTo (fun (x : ℂ) ↦ x + (↑l : ℂ)) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: refine (L.differentiableOn_weierstrassPExcept l₀).comp (f := (· + l.1)) (by fun_prop) ?_
-- 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
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
⊢ Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ))) x)
    (deriv
      (fun (x : ℂ) ↦ ℘[L - l₀ - (↑l : ℂ)] x + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
      x)
have simp : deriv ℘[L - l₀] (x + (↑l : ℂ)) = deriv ℘[L - l₀ - (↑l : ℂ)] x
Tactic: simp only [deriv_add_const', deriv_comp_add_const]
-- 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
x : ℂ
hx a : x ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
⊢ deriv ℘[L - l₀] (x + (↑l : ℂ)) = deriv ℘[L - l₀ - (↑l : ℂ)] x
have a₁ : x + (↑l : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
Tactic: rw [L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, L.derivWeierstrassPExcept_add_coe]
-- 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
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
⊢ x + (↑l : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
have a : ∀ (hx : x ∈ L.lattice → x + (↑l : ℂ) = l₀), x + (↑l : ℂ) ∈ L.lattice → x + (↑l : ℂ) = l₀
Tactic: simp only [Set.mem_compl_iff, Set.mem_diff, SetLike.mem_coe, Set.mem_singleton_iff, not_and,
        Decidable.not_not, eq_sub_iff_add_eq] at hx ⊢
Cleared hypotheses: hx
-- 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
⊢ ℘[L - l₀] (-((↑l : ℂ) / 2) + (↑l : ℂ)) =
    ℘[L - l₀ - (↑l : ℂ)] (-((↑l : ℂ) / 2)) + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2)
have rw : ℘[L] (-((↑l : ℂ) / 2) + (↑l : ℂ)) +
    (1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ) 2 -
      1 /
        HPow.hPow (β := ℕ) (-((↑l : ℂ) / 2) + (↑l : ℂ) - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ))
          2) =
  ℘[L] ((↑l : ℂ) / 2) +
    (1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) sorry) : ℂ) 2 -
        1 /
          HPow.hPow (β := ℕ)
            ((↑l : ℂ) / 2 - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) sorry) : ℂ)) 2 +
      (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
Tactic: rw [L.weierstrassPExcept_neg, L.weierstrassPExcept_def ⟨l₀, hl₀⟩,
      L.weierstrassPExcept_def ⟨_, neg_mem (sub_mem hl₀ l.2)⟩, add_assoc]
-- 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
⊢ ℘[L] (-((↑l : ℂ) / 2) + (↑l : ℂ)) +
      (1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ) 2 -
        1 /
          HPow.hPow (β := ℕ)
            (-((↑l : ℂ) / 2) + (↑l : ℂ) - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ)) 2) =
    ℘[L] ((↑l : ℂ) / 2) +
      (1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) ⋯) : ℂ) 2 -
          1 /
            HPow.hPow (β := ℕ)
              ((↑l : ℂ) / 2 - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) ⋯) : ℂ)) 2 +
        (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
have e_a : -((↑l : ℂ) / 2) + (↑l : ℂ) = (↑l : ℂ) / 2
Tactic: congr 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
e_a : -((↑l : ℂ) / 2) + (↑l : ℂ) = (↑l : ℂ) / 2
⊢ ℘[L] (-((↑l : ℂ) / 2) + (↑l : ℂ)) +
      (1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ) 2 -
        1 /
          HPow.hPow (β := ℕ)
            (-((↑l : ℂ) / 2) + (↑l : ℂ) - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ)) 2) =
    ℘[L] ((↑l : ℂ) / 2) +
      (1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) ⋯) : ℂ) 2 -
          1 /
            HPow.hPow (β := ℕ)
              ((↑l : ℂ) / 2 - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) ⋯) : ℂ)) 2 +
        (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2))
have e_a₁ : 1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ) 2 -
    1 /
      HPow.hPow (β := ℕ) (-((↑l : ℂ) / 2) + (↑l : ℂ) - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) l₀ hl₀) : ℂ))
        2 =
  1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) sorry) : ℂ) 2 -
      1 /
        HPow.hPow (β := ℕ) ((↑l : ℂ) / 2 - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (-(l₀ - (↑l : ℂ))) sorry) : ℂ))
          2 +
    (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have hl0 : l ≠ 0
Tactic: have hl0 : l ≠ 0 := by rintro rfl; simp at hl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have pos : ∀ (hz : z ∈ L.lattice), ℘[L] (z + (↑l : ℂ)) = ℘[L] z
Tactic: by_cases hz : z ∈ L.lattice
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
pos : ∀ (hz : z ∈ L.lattice), ℘[L] (z + (↑l : ℂ)) = ℘[L] z
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have neg : ∀ (hz : z ∉ L.lattice), ℘[L] (z + (↑l : ℂ)) = ℘[L] z
Tactic: by_cases hz : z ∈ L.lattice
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have this : Eq (α := ℂ) ((fun (x : ℂ) ↦ ℘[L - z + (↑l : ℂ)] (x + (↑l : ℂ))) z)
  ((fun (x : ℂ) ↦
      ℘[L - z + (↑l : ℂ) - (↑l : ℂ)] x +
        (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l : ℂ)) 2))
    z)
Tactic: have := L.weierstrassPExcept_add_coe_aux (z + l) (add_mem hz l.2) l hl (x := z) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this :
  ℘[L - z + (↑l : ℂ)] (z + (↑l : ℂ)) =
    ℘[L - z + (↑l : ℂ) - (↑l : ℂ)] z +
      (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l : ℂ)) 2)
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have pos : ℘[L - z + (↑l : ℂ) - (↑l : ℂ)] z +
      (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l : ℂ)) 2) +
    (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (z + (↑l : ℂ)) sorry) : ℂ)) 2 -
      1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (z + (↑l : ℂ)) sorry) : ℂ) 2) =
  ℘[L - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) z hz) : ℂ)] z +
    (1 / HPow.hPow (β := ℕ) (z - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) z hz) : ℂ)) 2 -
      1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) z hz) : ℂ) 2)
Tactic: rw [← L.weierstrassPExcept_add ⟨z + l, add_mem hz l.2⟩, this,
      ← L.weierstrassPExcept_add ⟨z, hz⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this :
  ℘[L - z + (↑l : ℂ)] (z + (↑l : ℂ)) =
    ℘[L - z + (↑l : ℂ) - (↑l : ℂ)] z +
      (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l : ℂ)) 2)
⊢ ℘[L - z + (↑l : ℂ) - (↑l : ℂ)] z +
        (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑l : ℂ)) 2) +
      (1 /
          HPow.hPow (β := ℕ) (z + (↑l : ℂ) - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (z + (↑l : ℂ)) ⋯) : ℂ))
            2 -
        1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) (z + (↑l : ℂ)) ⋯) : ℂ) 2) =
    ℘[L - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) z hz) : ℂ)] z +
      (1 / HPow.hPow (β := ℕ) (z - (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) z hz) : ℂ)) 2 -
        1 / HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℂ) ↦ x ∈ L.lattice) z hz) : ℂ) 2)
have pos : ℘[L - z] z + ((HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ - (HPow.hPow (β := ℕ) z 2)⁻¹) +
    -(HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ =
  ℘[L - z] z + -(HPow.hPow (β := ℕ) z 2)⁻¹
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have this : Eq (α := ℂ) ((fun (x : ℂ) ↦ ℘[L - 0] (x + (↑l : ℂ))) z)
  ((fun (x : ℂ) ↦
      ℘[L - 0 - (↑l : ℂ)] x + (1 / HPow.hPow (α := ℂ) (β := ℕ) 0 2 - 1 / HPow.hPow (β := ℕ) (0 - (↑l : ℂ)) 2))
    z)
Tactic: have := L.weierstrassPExcept_add_coe_aux 0 (zero_mem _) l hl (x := z) (by simp [hz])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this :
  Eq (α := ℂ) ((fun (x : ℂ) ↦ ℘[L - 0] (x + (↑l : ℂ))) z)
    ((fun (x : ℂ) ↦
        ℘[L - 0 - (↑l : ℂ)] x + (1 / HPow.hPow (α := ℂ) (β := ℕ) 0 2 - 1 / HPow.hPow (β := ℕ) (0 - (↑l : ℂ)) 2))
      z)
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have this₁ : ℘[L - 0] (z + (↑l : ℂ)) = ℘[L - -(↑l : ℂ)] z + -(HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹
Tactic: simp only [zero_sub, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, div_zero,
      even_two, Even.neg_pow, one_div] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + (↑l : ℂ)) = ℘[L - -(↑l : ℂ)] z + -(HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have neg : ℘[L - -(↑l : ℂ)] z + -(HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹ +
    (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - 0) 2 - 1 / HPow.hPow (α := ℂ) (β := ℕ) 0 2) =
  ℘[L - (↑(-l) : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑(-l) : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑(-l) : ℂ) 2)
Tactic: rw [← L.weierstrassPExcept_add 0, Submodule.coe_zero, this, ← L.weierstrassPExcept_add (-l)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + (↑l : ℂ)) = ℘[L - -(↑l : ℂ)] z + -(HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹
⊢ ℘[L - -(↑l : ℂ)] z + -(HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹ +
      (1 / HPow.hPow (β := ℕ) (z + (↑l : ℂ) - 0) 2 - 1 / HPow.hPow (α := ℂ) (β := ℕ) 0 2) =
    ℘[L - (↑(-l) : ℂ)] z + (1 / HPow.hPow (β := ℕ) (z - (↑(-l) : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑(-l) : ℂ) 2)
have neg : ℘[L - -(↑l : ℂ)] z + -(HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹ + (HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ =
  ℘[L - -(↑l : ℂ)] z + ((HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ - (HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹)
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
| ℘[L] (i + -z)
have rw : (fun (x : ℂ) ↦ ℘[L] (x + z)) (i + -z)
Tactic: rw [← hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
| (fun (x : ℂ) ↦ ℘[L] (x + z)) (i + -z)
have simp : ℘[L] i
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
| ℘[L] (i + -z)
have rw : ℘[L] i
Tactic: rw [← hz]; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
⊢ ℘[L] (i + -z) = ℘[L] i
have conv_lhs : ℘[L] (i + -z) = ℘[L] i
Tactic: conv_lhs => rw [← hz]; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
conv_lhs : ℘[L] (i + -z) = ℘[L] i
⊢ ℘[L] (i + -z) = ℘[L] i
have conv_lhs₁ : ℘[L] i = ℘[L] i
Tactic: conv_lhs => rw [← hz]; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ L.lattice ≤ (AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G
have rw : {L.ω₁, L.ω₂} ⊆ (↑((AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G : Submodule ℤ ℂ) : Set ℂ)
Tactic: rw [lattice, Submodule.span_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ L.ω₁ ∈ (↑((AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G : Submodule ℤ ℂ) : Set ℂ)
have inl : ∀ (i : ℂ), ℘[L] (i + L.ω₁) = ℘[L] i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ L.ω₂ ∈ (↑((AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G : Submodule ℤ ℂ) : Set ℂ)
have inr : ∀ (i : ℂ), ℘[L] (i + L.ω₂) = ℘[L] i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z
have this : L.lattice ≤ (AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G
Tactic: have : L.lattice ≤ G.toIntSubmodule := by
    rw [lattice, Submodule.span_le]
    rintro _ (rfl | rfl)
    · ext i
      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice
    · ext i
      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ↥L.lattice
⊢ ℘[L] (↑l : ℂ) = 0
have rw : ℘[L] (0 + (↑l : ℂ)) = 0
Tactic: rw [← zero_add l.1, L.weierstrassP_add_coe, L.weierstrassP_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ↥L.lattice
rw : ℘[L] (0 + (↑l : ℂ)) = 0
⊢ ℘[L] (↑l : ℂ) = 0
have rw₁ : ℘[L] 0 = 0
Tactic: rw [← zero_add l.1, L.weierstrassP_add_coe, L.weierstrassP_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l : ↥L.lattice
rw : ℘[L] (0 + (↑l : ℂ)) = 0
rw₁ : ℘[L] 0 = 0
⊢ ℘[L] (↑l : ℂ) = 0
have rw₂ : Eq (α := ℂ) 0 0
Tactic: rw [← zero_add l.1, L.weierstrassP_add_coe, L.weierstrassP_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘[L] (z - (↑l : ℂ)) = ℘[L] z
have rw : ℘[L] (z - (↑l : ℂ) + (↑l : ℂ)) = ℘[L] z
Tactic: rw [← L.weierstrassP_add_coe _ l, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
rw : ℘[L] (z - (↑l : ℂ) + (↑l : ℂ)) = ℘[L] z
⊢ ℘[L] (z - (↑l : ℂ)) = ℘[L] z
have rw₁ : ℘[L] z = ℘[L] z
Tactic: rw [← L.weierstrassP_add_coe _ l, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 = ℘'[L] z
have trans : ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 =
  ℘'[L - (↑l₀ : ℂ)] z +
    ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0
Tactic: trans ℘'[L - l₀] z + ∑' i : L.lattice, if i.1 = l₀.1 then (- 2 / (z - l₀) ^ 3) else 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
trans :
  ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 =
    ℘'[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0
⊢ ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 = ℘'[L] z
have trans₁ : (℘'[L - (↑l₀ : ℂ)] z +
    ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
  ℘'[L] z
Tactic: trans ℘'[L - l₀] z + ∑' i : L.lattice, if i.1 = l₀.1 then (- 2 / (z - l₀) ^ 3) else 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ (℘'[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    ℘'[L] z
have rw : Eq (α := ℂ)
  (∑' (b : ↥L.lattice),
    ((if (↑b : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3) +
      if (↑b : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0))
  (∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3))
Tactic: rw [derivWeierstrassP, derivWeierstrassPExcept, ← Summable.tsum_add, ← tsum_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
rw :
  Eq (α := ℂ)
    (∑' (b : ↥L.lattice),
      ((if (↑b : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3) +
        if (↑b : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0))
    (∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3))
⊢ (℘'[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    ℘'[L] z
have hf : Summable (α := ℂ) fun (l : ↥L.lattice) ↦ if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
Tactic: rw [derivWeierstrassP, derivWeierstrassPExcept, ← Summable.tsum_add, ← tsum_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
rw :
  Eq (α := ℂ)
    (∑' (b : ↥L.lattice),
      ((if (↑b : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3) +
        if (↑b : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0))
    (∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3))
hf :
  Summable (α := ℂ) fun (l : ↥L.lattice) ↦ if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
⊢ (℘'[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    ℘'[L] z
have hg : Summable (α := ℂ) fun (i : ↥L.lattice) ↦ if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0
Tactic: rw [derivWeierstrassP, derivWeierstrassPExcept, ← Summable.tsum_add, ← tsum_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Eq (α := ℂ)
    (∑' (b : ↥L.lattice),
      ((if (↑b : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3) +
        if (↑b : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0))
    (∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3))
have e_f : ∀ (w : ↥L.lattice),
  ((if (↑w : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3) +
      if (↑w : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)
Tactic: congr with w
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
⊢ ((if (↑w : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3) +
      if (↑w : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)
have pos : (↑w : ℂ) = (↑l₀ : ℂ) → 0 + -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 = -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
pos : (↑w : ℂ) = (↑l₀ : ℂ) → 0 + -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 = -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)
⊢ ((if (↑w : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3) +
      if (↑w : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)
have neg : ¬(↑w : ℂ) = (↑l₀ : ℂ) → -2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3 + 0 = -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)
Tactic: split_ifs