awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (↑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
neg :
  -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
    HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2) l) 0
⊢ -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
    deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l

Tactic:
rw [deriv_fun_sub (.fun_div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop),
        deriv_const]

Premises used: deriv_fun_sub, deriv_const
-- 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
neg :
  -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 =
    HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ HPow.hPow (β := ℤ) (x2 - (↑x : ℂ)) (-2)) l) 0
⊢ -2 / HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 3 =
    HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2) l) 0

Tactic:
simp_rw [← zpow_natCast, one_div, ← zpow_neg, Nat.cast_ofNat]

Premises used: zpow_natCast, Nat.cast_ofNat, zpow_neg, one_div
-- 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
neg : -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 = (↑(-2) : ℂ) * (l - (↑x : ℂ)) ^ HSub.hSub (α := ℤ) (-2) 1 - 0
⊢ -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 =
    HSub.hSub (α := ℂ) (deriv (fun (x2 : ℂ) ↦ HPow.hPow (β := ℤ) (x2 - (↑x : ℂ)) (-2)) l) 0

Tactic:
rw [deriv_comp_sub_const (f := (· ^ (-2 : ℤ))), deriv_zpow]

Premises used: deriv_zpow, HPow.hPow, OfNat.ofNat, Neg.neg, deriv_comp_sub_const
-- 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
neg : -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 = -(2 * (HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3)⁻¹)
⊢ -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 = (↑(-2) : ℂ) * (l - (↑x : ℂ)) ^ HSub.hSub (α := ℤ) (-2) 1 - 0

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₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ -2 / HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3 = -(2 * (HPow.hPow (β := ℤ) (l - (↑x : ℂ)) 3)⁻¹)

Tactic:
field_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
hxs : x ∈ s
pos : ∀ (hl₁ : (↑x : ℂ) = l₀), DifferentiableAt ℂ (F := ℂ) (fun (x2 : ℂ) ↦ 0) l
neg :
  ∀ (hl₁ : ¬(↑x : ℂ) = l₀),
    DifferentiableAt ℂ (F := ℂ)
      (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l
⊢ DifferentiableAt ℂ (F := ℂ)
    (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
hxs : x ∈ s
hl₁ : (↑x : ℂ) = l₀
⊢ DifferentiableAt ℂ (F := ℂ) (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
hxs : x ∈ s
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
hxs : x ∈ s
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
hxs : x ∈ s
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
hxs : x ∈ s
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
hxs : x ∈ s
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x2 : ℂ) ↦ 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
hxs : x ∈ s
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x2 : ℂ) ↦ HPow.hPow (β := ℕ) (x2 - (↑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
hxs : x ∈ s
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ HPow.hPow (β := ℕ) (l - (↑x : ℂ)) 2 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (↑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
hxs : x ∈ s
hl₁_1 : ¬(↑x : ℂ) = l₀
hl₁ : l - (↑x : ℂ) ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x2 : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (x2 - (↑x : ℂ)) 2 - 1 / HPow.hPow (β := ℕ) (↑x : ℂ) 2) l

Tactic:
exact .sub (.div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
⊢ l ∈ ((↑L.lattice : Set ℂ) \ {l})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
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)
⊢ 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)

Tactic:
rw [← (Equiv.neg L.lattice).tsum_eq]

Premises used: Equiv.neg, Equiv.tsum_eq, Membership.mem, Subtype, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
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)
⊢ 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:
simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub,
    ← div_neg, ← tsum_neg, apply_ite, neg_zero]

Premises used: neg_add_eq_sub, apply_ite, Equiv.neg_apply, div_neg, tsum_neg, neg_zero, sub_neg_eq_add, NegMemClass.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
h : ∀ (l : ↥L.lattice), -(↑l : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀
h₁ :
  ∀ (l : ↥L.lattice),
    ¬(↑l : ℂ) = -l₀ → -2 / HPow.hPow (β := ℕ) ((↑l : ℂ) - z) 3 = -2 / -HPow.hPow (β := ℕ) (z - (↑l : ℂ)) 3
⊢ 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:
congr! 3 with l
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ -(↑l : ℂ) = l₀ ↔ (↑l : ℂ) = -l₀

Tactic:
simp [neg_eq_iff_eq_neg]

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

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ ℘'[L - 0] 0 = 0

Tactic:
simpa [CharZero.eq_neg_self_iff] using L.derivWeierstrassPExcept_neg 0 0

Premises used: CharZero.eq_neg_self_iff, PeriodPair.derivWeierstrassPExcept_neg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
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)
⊢ 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)

Tactic:
rw [← (Equiv.addRight l).tsum_eq]

Premises used: Equiv.addRight, Equiv.tsum_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ 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:
simp only [Equiv.coe_addRight, Submodule.coe_add, add_sub_add_right_eq_sub, eq_sub_iff_add_eq]

Premises used: Submodule.coe_add, eq_sub_iff_add_eq, Equiv.coe_addRight, add_sub_add_right_eq_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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 : ℂ)})ᶜ
apply₅ :
  ℘[L - l₀] (-((↑l : ℂ) / 2) + (↑l : ℂ)) =
    ℘[L - l₀ - (↑l : ℂ)] (-((↑l : ℂ) / 2)) + (1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2)
⊢ 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 : ℂ)})ᶜ

Tactic:
apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_diff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_

Premises used: PeriodPair.isOpen_compl_lattice_diff, IsOpen.eqOn_of_deriv_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ 1 < Module.rank ℝ ℂ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
refine : ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)}).Countable
⊢ IsPreconnected ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ

Tactic:
refine (Set.Countable.isConnected_compl_of_one_lt_rank (by simp) ?_).2

Premises used: Set.Countable.isConnected_compl_of_one_lt_rank, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)}).Countable

Tactic:
.mono sdiff_le (countable_of_Lindelof_of_discrete (X := L.lattice))

Premises used: countable_of_Lindelof_of_discrete, sdiff_le, Set.Countable.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)}).Countable

Tactic:
exact .mono sdiff_le (countable_of_Lindelof_of_discrete (X := L.lattice))
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ x + (↑l : ℂ)) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
refine :
  Set.MapsTo (fun (x : ℂ) ↦ x + (↑l : ℂ)) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ ℘[L - l₀] (x + (↑l : ℂ))) ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ

Tactic:
refine (L.differentiableOn_weierstrassPExcept l₀).comp (f := (· + l.1)) (by fun_prop) ?_

Premises used: PeriodPair.differentiableOn_weierstrassPExcept, DifferentiableOn.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
x : ℂ
h₁ : x ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
h₂ : x + (↑l : ℂ) ∈ (↑L.lattice : Set ℂ)
h₃ : x + (↑l : ℂ) ≠ l₀
⊢ x ∈ (↑L.lattice : Set ℂ)

Tactic:
simpa using sub_mem h₂ l.2

Premises used: sub_mem, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
h₁ : l₀ - (↑l : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
h₂ : l₀ - (↑l : ℂ) + (↑l : ℂ) ∈ (↑L.lattice : Set ℂ)
h₃ : l₀ - (↑l : ℂ) + (↑l : ℂ) ≠ l₀
⊢ False

Tactic:
simp at h₃
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
x : ℂ
h₁ : x ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
h₂ : x + (↑l : ℂ) ∈ (↑L.lattice : Set ℂ)
h₃ : x + (↑l : ℂ) ≠ l₀
⊢ False

Tactic:
exact h₁ ⟨by simpa using sub_mem h₂ l.2, by rintro rfl; simp at h₃⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ 1 / HPow.hPow (β := ℕ) l₀ 2 - 1 / HPow.hPow (β := ℕ) (l₀ - (↑l : ℂ)) 2)
    ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ 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:
refine .add (L.differentiableOn_weierstrassPExcept _) (by simp)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
simp : deriv ℘[L - l₀] (x + (↑l : ℂ)) = deriv ℘[L - l₀ - (↑l : ℂ)] x
⊢ 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)

Tactic:
simp only [deriv_add_const', deriv_comp_add_const]

Premises used: deriv_comp_add_const, deriv_add_const'
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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 : ℂ)})ᶜ
a₁ : x + (↑l : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ deriv ℘[L - l₀] (x + (↑l : ℂ)) = deriv ℘[L - l₀ - (↑l : ℂ)] x

Tactic:
rw [L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, L.derivWeierstrassPExcept_add_coe]

Premises used: PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, PeriodPair.derivWeierstrassPExcept_add_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
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.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
x : ℂ
hx : x ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ
a : ∀ (hx : x ∈ L.lattice → x + (↑l : ℂ) = l₀), x + (↑l : ℂ) ∈ L.lattice → x + (↑l : ℂ) = l₀
⊢ x + (↑l : ℂ) ∈ ((↑L.lattice : Set ℂ) \ {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 ⊢

Premises used: eq_sub_iff_add_eq, Set.mem_singleton_iff, SetLike.mem_coe, Set.mem_diff, Decidable.not_not, not_and, Set.mem_compl_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
x : ℂ
hx : x ∈ L.lattice → x + (↑l : ℂ) = l₀
H : x + (↑l : ℂ) ∈ L.lattice
⊢ x ∈ L.lattice

Tactic:
simpa using sub_mem H l.2

Premises used: sub_mem, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
x : ℂ
hx : x ∈ L.lattice → x + (↑l : ℂ) = l₀
⊢ x + (↑l : ℂ) ∈ L.lattice → x + (↑l : ℂ) = l₀

Tactic:
exact fun H ↦ hx (by simpa using sub_mem H l.2)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ -((↑l : ℂ) / 2) ∈ ((↑L.lattice : Set ℂ) \ {l₀ - (↑l : ℂ)})ᶜ

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

Premises used: add_assoc, PeriodPair.weierstrassPExcept_neg, PeriodPair.weierstrassPExcept_def, sub_mem, Subtype.mk, Subtype.property, NegMemClass.neg_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
e_a : -((↑l : ℂ) / 2) + (↑l : ℂ) = (↑l : ℂ) / 2
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 : ℂ))) ⋯) : ℂ) 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)
⊢ ℘[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))

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ -((↑l : ℂ) / 2) + (↑l : ℂ) = (↑l : ℂ) / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ 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 : ℂ))) ⋯) : ℂ) 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)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hl : HDiv.hDiv (α := ℂ) (↑0 : ℂ) 2 ∉ L.lattice
⊢ False

Tactic:
simp at hl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : (↑l : ℂ) / 2 ∉ L.lattice
⊢ l ≠ 0

Tactic:
have hl0 : l ≠ 0 := by rintro rfl; simp at hl