awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
neg : ∀ (hz : z ∉ L.lattice), ℘[L] (z + (↑l : ℂ)) = ℘[L] z
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z

Tactic:
by_cases hz : z ∈ L.lattice

Premises used: PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
⊢ z ∈ ((↑L.lattice : Set ℂ) \ {z + (↑l : ℂ) - (↑l : ℂ)})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)
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 : ℂ)) ⋯) : ℂ))
            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)
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z

Tactic:
rw [← L.weierstrassPExcept_add ⟨z + l, add_mem hz l.2⟩, this,
      ← L.weierstrassPExcept_add ⟨z, hz⟩]

Premises used: Subtype.mk, HAdd.hAdd, AddMemClass.add_mem, Subtype.val, Subtype.property, PeriodPair.weierstrassPExcept_add
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)
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)⁻¹
⊢ ℘[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)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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] z + ((HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ - (HPow.hPow (β := ℕ) z 2)⁻¹) +
      -(HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ =
    ℘[L - z] z + -(HPow.hPow (β := ℕ) z 2)⁻¹

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
⊢ z ∈ ((↑L.lattice : Set ℂ) \ {0 - (↑l : ℂ)})ᶜ

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
⊢ 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])
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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 - 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

Premises used: OfNat.ofNat_ne_zero, even_two, Even.neg_pow, ne_eq, one_div, not_false_eq_true, div_zero, zero_pow, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)⁻¹
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)
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z

Tactic:
rw [← L.weierstrassPExcept_add 0, Submodule.coe_zero, this, ← L.weierstrassPExcept_add (-l)]

Premises used: Submodule.coe_zero, OfNat.ofNat, Neg.neg, PeriodPair.weierstrassPExcept_add
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)⁻¹
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)⁻¹)
⊢ ℘[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:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)⁻¹ + (HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ =
    ℘[L - -(↑l : ℂ)] z + ((HPow.hPow (β := ℕ) (z + (↑l : ℂ)) 2)⁻¹ - (HPow.hPow (β := ℕ) (↑l : ℂ) 2)⁻¹)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ∀ {a b : ℂ},
    Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} a →
      Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} b →
        Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} (a + b)

Tactic:
simp_all [funext_iff, ← add_assoc]

Premises used: add_assoc, funext_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
rw : (fun (x : ℂ) ↦ ℘[L] (x + z)) (i + -z)
| ℘[L] (i + -z)

Tactic:
rw [← hz]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
simp : ℘[L] i
| (fun (x : ℂ) ↦ ℘[L] (x + z)) (i + -z)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z_1 : ℂ
l : ↥L.lattice
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]} z
i : ℂ
rw : ℘[L] i
| ℘[L] (i + -z)

Tactic:
rw [← hz]; simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
conv_lhs₁ : ℘[L] i = ℘[L] i
⊢ ℘[L] (i + -z) = ℘[L] i

Tactic:
conv_lhs => rw [← hz]; simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
rw : {L.ω₁, L.ω₂} ⊆ (↑((AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G : Submodule ℤ ℂ) : Set ℂ)
⊢ L.lattice ≤ (AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G

Tactic:
rw [lattice, Submodule.span_le]

Premises used: PeriodPair.lattice, Submodule.span_le
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
inl : ∀ (i : ℂ), ℘[L] (i + L.ω₁) = ℘[L] i
⊢ L.ω₁ ∈ (↑((AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G : Submodule ℤ ℂ) : Set ℂ)

Tactic:
ext i
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
i : ℂ
⊢ ℘[L] (i + L.ω₁) = ℘[L] i

Tactic:
L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, Subtype.mk, _private.0.PeriodPair.weierstrassP_add_coe_aux, PeriodPair.ω₁_mem_lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
i : ℂ
⊢ ℘[L] (i + L.ω₁) = ℘[L] i

Tactic:
exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, Subtype.mk, _private.0.PeriodPair.weierstrassP_add_coe_aux, PeriodPair.ω₁_mem_lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
inr : ∀ (i : ℂ), ℘[L] (i + L.ω₂) = ℘[L] i
⊢ L.ω₂ ∈ (↑((AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G : Submodule ℤ ℂ) : Set ℂ)

Tactic:
ext i
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
i : ℂ
⊢ ℘[L] (i + L.ω₂) = ℘[L] i

Tactic:
L.weierstrassP_add_coe_aux _ ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice

Premises used: PeriodPair.ω₂_div_two_notMem_lattice, Subtype.mk, _private.0.PeriodPair.weierstrassP_add_coe_aux, PeriodPair.ω₂_mem_lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
i : ℂ
⊢ ℘[L] (i + L.ω₂) = ℘[L] i

Tactic:
exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice

Premises used: PeriodPair.ω₂_div_two_notMem_lattice, Subtype.mk, _private.0.PeriodPair.weierstrassP_add_coe_aux, PeriodPair.ω₂_mem_lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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

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
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
this : L.lattice ≤ (AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z

Tactic:
congr_fun (this l.2) _

Premises used: congr_fun, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ :=
  { carrier := {z : ℂ | (fun (x : ℂ) ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
this : L.lattice ≤ (AddSubgroup.toIntSubmodule : (a : AddSubgroup ℂ) → Submodule ℤ ℂ) G
⊢ ℘[L] (z + (↑l : ℂ)) = ℘[L] z

Tactic:
exact congr_fun (this l.2) _

Premises used: congr_fun, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
⊢ Function.Periodic ℘[L] (↑l : ℂ)

Tactic:
(L.weierstrassP_add_coe · l)

Premises used: PeriodPair.weierstrassP_add_coe, Function.Periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ ℘[L] 0 = 0

Tactic:
simp [weierstrassP]

Premises used: PeriodPair.weierstrassP
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
rw : ℘[L] (0 + (↑l : ℂ)) = 0
rw₁ : ℘[L] 0 = 0
rw₂ rw₃ : Eq (α := ℂ) 0 0
⊢ ℘[L] (↑l : ℂ) = 0

Tactic:
rw [← zero_add l.1, L.weierstrassP_add_coe, L.weierstrassP_zero]

Premises used: PeriodPair.weierstrassP_zero, zero_add, PeriodPair.weierstrassP_add_coe, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
rw : ℘[L] (z - (↑l : ℂ) + (↑l : ℂ)) = ℘[L] z
rw₁ rw₂ : ℘[L] z = ℘[L] z
⊢ ℘[L] (z - (↑l : ℂ)) = ℘[L] z

Tactic:
rw [← L.weierstrassP_add_coe _ l, sub_add_cancel]

Premises used: PeriodPair.weierstrassP_add_coe, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
trans₁ :
  (℘'[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    ℘'[L] z
⊢ ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 = ℘'[L] z

Tactic:
trans ℘'[L - l₀] z + ∑' i : L.lattice, if i.1 = l₀.1 then (- 2 / (z - l₀) ^ 3) else 0

Premises used: HSub.hSub, HDiv.hDiv, PeriodPair.derivWeierstrassPExcept, HPow.hPow, OfNat.ofNat, Subtype.val, PeriodPair.lattice, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[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:
simp [sub_eq_add_neg, neg_div]

Premises used: neg_div, sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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
hg :
  Summable (α := ℂ) fun (i : ↥L.lattice) ↦ if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0
⊢ (℘'[L - (↑l₀ : ℂ)] z +
      ∑' (i : ↥L.lattice), if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0) =
    ℘'[L] z

Tactic:
rw [derivWeierstrassP, derivWeierstrassPExcept, ← Summable.tsum_add, ← tsum_neg]

Premises used: PeriodPair.derivWeierstrassPExcept, tsum_neg, PeriodPair.derivWeierstrassP, Summable.tsum_add
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
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)
⊢ 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:
congr with w
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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)
neg : ¬(↑w : ℂ) = (↑l₀ : ℂ) → -2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3 + 0 = -(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)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h : (↑w : ℂ) = (↑l₀ : ℂ)
⊢ 0 + -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 = -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)

Tactic:
simp only [zero_add, add_zero, *, neg_div]

Premises used: neg_div, zero_add, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h : ¬(↑w : ℂ) = (↑l₀ : ℂ)
⊢ -2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3 + 0 = -(2 / HPow.hPow (β := ℕ) (z - (↑w : ℂ)) 3)

Tactic:
simp only [zero_add, add_zero, *, neg_div]

Premises used: neg_div, zero_add, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable (α := ℂ) fun (l : ↥L.lattice) ↦ if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3

Tactic:
⟨_, L.hasSum_derivWeierstrassPExcept _ _⟩

Premises used: PeriodPair.hasSum_derivWeierstrassPExcept, Exists.intro, Summable
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable (α := ℂ) fun (l : ↥L.lattice) ↦ if (↑l : ℂ) = (↑l₀ : ℂ) then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3

Tactic:
exact ⟨_, L.hasSum_derivWeierstrassPExcept _ _⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Subset (α := Set ↥L.lattice)
    (Function.support (M := ℂ) fun (i : ↥L.lattice) ↦
      if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0)
    {l₀}

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable (α := ℂ) fun (i : ↥L.lattice) ↦ if (↑i : ℂ) = (↑l₀ : ℂ) then -2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 else 0

Tactic:
exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

Premises used: Set.Finite.subset, summable_of_hasFiniteSupport, Set.finite_singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
rw :
  ℘'[L - (↑l₀ : ℂ)] z =
    ℘'[L - (↑l₀ : ℂ)] z - 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3 + 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3
rw₁ rw₂ : ℘'[L - (↑l₀ : ℂ)] z = ℘'[L - (↑l₀ : ℂ)] z
⊢ ℘'[L - (↑l₀ : ℂ)] z = ℘'[L] z + 2 / HPow.hPow (β := ℕ) (z - (↑l₀ : ℂ)) 3

Tactic:
rw [← L.derivWeierstrassPExcept_sub l₀, sub_add_cancel]

Premises used: PeriodPair.derivWeierstrassPExcept_sub, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
simp_rw :
  Eq (α := (z : ℂ) → ℂ)
    (fun (z : ℂ) ↦ ∑' (l : ↥L.lattice), if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
    fun (z : ℂ) ↦ ∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)
⊢ Eq (α := (z : ℂ) → ℂ)
    (fun (z : ℂ) ↦ ∑' (l : ↥L.lattice), if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
    fun (z : ℂ) ↦ -∑' (l : ↥L.lattice), 2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3

Tactic:
simp_rw [← tsum_neg]

Premises used: tsum_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
h :
  ∀ (z : ℂ) (l : ↥L.lattice),
    (if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) = -(2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
⊢ Eq (α := (z : ℂ) → ℂ)
    (fun (z : ℂ) ↦ ∑' (l : ↥L.lattice), if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)
    fun (z : ℂ) ↦ ∑' (b : ↥L.lattice), -(2 / HPow.hPow (β := ℕ) (z - (↑b : ℂ)) 3)

Tactic:
congr! 3 with z l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
z : ℂ
l : ↥L.lattice
this : (↑l : ℂ) ≠ l₀
⊢ (if (↑l : ℂ) = l₀ then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) = -(2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3)

Tactic:
simp [this, neg_div]

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

Tactic:
L.hasSumLocallyUniformly_derivWeierstrassPExcept (L.ω₁ / 2)

Premises used: HDiv.hDiv, PeriodPair.ω₁, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
h :
  ∀ (l : ↥L.lattice) (z : ℂ),
    -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3 =
      if (↑l : ℂ) = L.ω₁ / 2 then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
h₁ : ℘'[L] = ℘'[L - L.ω₁ / 2]
⊢ HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) ↦ -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3) ℘'[L]

Tactic:
convert! L.hasSumLocallyUniformly_derivWeierstrassPExcept (L.ω₁ / 2) using 3 with l z

Premises used: HDiv.hDiv, PeriodPair.ω₁, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
z : ℂ
h : ¬(↑l : ℂ) = L.ω₁ / 2
⊢ -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3 = if (↑l : ℂ) = L.ω₁ / 2 then 0 else -2 / HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3

Tactic:
rw [if_neg, neg_div]

Premises used: neg_div, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ ¬(↑l : ℂ) = L.ω₁ / 2

Tactic:
fun e ↦ L.ω₁_div_two_notMem_lattice (e ▸ l.2)

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, Eq.rec, Not, Subtype.property