awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
rw :
  LE.le (α := WithTop ℤ) 7
    (ENat.map Nat.cast (analyticOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0))
⊢ 7 ≤ meromorphicOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0

Tactic:
rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop)]

Premises used: AnalyticAt.meromorphicOrderAt_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
refine : ∀ (i : ℕ) (hi₁ : i < 7), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
⊢ LE.le (α := WithTop ℤ) 7
    (ENat.map Nat.cast (analyticOrderAt (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0))

Tactic:
refine ENat.monotone_map_iff.mpr Nat.mono_cast
    ((natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (by fun_prop)).mpr fun i hi₁ ↦ ?_)

Premises used: Iff.mpr, ENat.monotone_map_iff, Nat.mono_cast, natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
pos : ∀ (hi₂ : Odd i), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
neg : ∀ (hi₂ : ¬Odd i), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
by_cases hi₂ : Odd i

Premises used: Odd
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : Odd i
⊢ Even (α := ℕ) 6

Tactic:
decide
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : Odd i
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
simpa [← CharZero.eq_neg_self_iff, hi₂, (show Even 6 by decide).neg_pow] using
      (iteratedDeriv_comp_neg i (L.relation * id ^ 6) 0 :)

Premises used: HMul.hMul, Even.neg_pow, id, iteratedDeriv_comp_neg, CharZero.eq_neg_self_iff, HPow.hPow, _private.0.PeriodPair.relation, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
pos : ∀ (hi₃ : i = 0), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
neg : ∀ (hi₃ : ¬i = 0), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
by_cases hi₃ : i = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : i = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
simp [hi₃]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
pos : ∀ (hi₄ : i = 6), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
neg : ∀ (hi₄ : ¬i = 6), iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
by_cases hi₄ : i = 6
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : i = 6
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
hi₄ ▸ L.iteratedDeriv_six_relation_mul_id_pow_six

Premises used: _private.0.PeriodPair.iteratedDeriv_six_relation_mul_id_pow_six, Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : i = 6
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
exact hi₄ ▸ L.iteratedDeriv_six_relation_mul_id_pow_six
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
neg :
  Eq (α := ℂ)
    (iteratedDeriv i
      (fun (z : ℂ) ↦
        HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
              4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
            L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
          L.g₃ * HPow.hPow (β := ℕ) z 6)
      0)
    0
⊢ iteratedDeriv i (L.relation * HPow.hPow (α := (a : ℂ) → ℂ) (β := ℕ) id 6) 0 = 0

Tactic:
rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]

Premises used: _private.0.PeriodPair.relation_mul_id_pow_six_eventuallyEq, Filter.EventuallyEq.iteratedDeriv_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
neg :
  Eq (α := ℂ)
    (iteratedDeriv i
      (fun (z : ℂ) ↦
        (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) * (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) -
              4 *
                ((℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) * (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) *
                  (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1)) +
            L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
          L.g₃ * HPow.hPow (β := ℕ) z 6)
      0)
    0
⊢ Eq (α := ℂ)
    (iteratedDeriv i
      (fun (z : ℂ) ↦
        HPow.hPow (β := ℕ) (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) 2 -
              4 * HPow.hPow (β := ℕ) (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) 3 +
            L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
          L.g₃ * HPow.hPow (β := ℕ) z 6)
      0)
    0

Tactic:
simp_rw [pow_succ (_ + _), pow_succ (_ - _), pow_zero, one_mul]

Premises used: pow_succ, HSub.hSub, pow_zero, HAdd.hAdd, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ i = 2 ∨ i = 4

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
hi₁ : 2 < 7
hi₂ : ¬Odd (α := ℕ) 2
hi₃ : ¬Eq (α := ℕ) 2 0
hi₄ : ¬Eq (α := ℕ) 2 6
⊢ HSub.hSub (α := ℂ)
          (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
            (↑(Nat.choose 2 x) : ℂ) *
                HSub.hSub (α := ℂ)
                  (∑ x_1 ∈ Finset.range (x + 1),
                    (↑(x.choose x_1) : ℂ) * ((↑(x_1 + 2)! : ℂ) * L.sumInvPow 0 (x_1 + 3)) *
                      (↑(if x - x_1 = 3 then 3! else 0) : ℂ))
                  (if x = 0 then 2 else 0) *
              HSub.hSub (α := ℂ)
                (∑ x_1 ∈ Finset.range (2 - x + 1),
                  (↑((2 - x).choose x_1) : ℂ) * ((↑(x_1 + 2)! : ℂ) * L.sumInvPow 0 (x_1 + 3)) *
                    (↑(if 2 - x - x_1 = 3 then 3! else 0) : ℂ))
                (if 2 - x = 0 then 2 else 0))
          (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
            HMul.hMul (α := ℂ) (↑(Nat.choose 2 x) : ℂ) (if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (2 - x + 1),
                HMul.hMul (α := ℂ) (↑((2 - x).choose x_1) : ℂ)
                    (∑ x ∈ Finset.range (x_1 + 1),
                      (↑(x_1.choose x) : ℂ) *
                          HAdd.hAdd (α := ℂ)
                            (∑ x_2 ∈ Finset.range (x + 1),
                              ((↑(x.choose x_2) : ℂ) *
                                  if x_2 = 0 then ℘[L - 0] 0 else (↑(x_2 + 1)! : ℂ) * L.sumInvPow 0 (x_2 + 2)) *
                                (↑(if x - x_2 = 2 then 2! else 0) : ℂ))
                            (if x = 0 then 1 else 0) *
                        HAdd.hAdd (α := ℂ)
                          (∑ x_2 ∈ Finset.range (x_1 - x + 1),
                            ((↑((x_1 - x).choose x_2) : ℂ) *
                                if x_2 = 0 then ℘[L - 0] 0 else (↑(x_2 + 1)! : ℂ) * L.sumInvPow 0 (x_2 + 2)) *
                              (↑(if x_1 - x - x_2 = 2 then 2! else 0) : ℂ))
                          (if x_1 - x = 0 then 1 else 0)) *
                  HAdd.hAdd (α := ℂ)
                    (∑ x_2 ∈ Finset.range (2 - x - x_1 + 1),
                      ((↑((2 - x - x_1).choose x_2) : ℂ) *
                          if x_2 = 0 then ℘[L - 0] 0 else (↑(x_2 + 1)! : ℂ) * L.sumInvPow 0 (x_2 + 2)) *
                        (↑(if 2 - x - x_1 - x_2 = 2 then 2! else 0) : ℂ))
                    (if 2 - x - x_1 = 0 then 1 else 0)) +
        ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
          ((↑(Nat.choose 2 x) : ℂ) * if x = 0 then L.g₂ else 0) *
            HAdd.hAdd (α := ℂ)
              (∑ x_1 ∈ Finset.range (2 - x + 1),
                ((↑((2 - x).choose x_1) : ℂ) *
                    if x_1 = 0 then ℘[L - 0] 0 else (↑(x_1 + 1)! : ℂ) * L.sumInvPow 0 (x_1 + 2)) *
                  (↑(if 2 - x - x_1 = 6 then 6! else 0) : ℂ))
              (↑(if 2 - x = 4 then 4! else 0) : ℂ) +
      ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
        ((↑(Nat.choose 2 x) : ℂ) * if x = 0 then L.g₃ else 0) * (↑(if 2 - x = 6 then 6! else 0) : ℂ) =
    0

Tactic:
simp [Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd (α := ℕ) 4
hi₃ : ¬Eq (α := ℕ) 4 0
hi₄ : ¬Eq (α := ℕ) 4 6
⊢ Nat.choose 4 2 = 6

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd (α := ℕ) 4
hi₃ : ¬Eq (α := ℕ) 4 0
hi₄ : ¬Eq (α := ℕ) 4 6
⊢ -(2 * (4 * ((↑3! : ℂ) * L.G 4) * (↑3! : ℂ))) + -(4 * ((↑3! : ℂ) * L.G 4) * (↑3! : ℂ) * 2) -
        4 * (6 * ((↑3! : ℂ) * L.G 4) * 2 + (6 * ((↑3! : ℂ) * L.G 4) * 2 + 6 * ((↑3! : ℂ) * L.G 4) * 2)) +
      60 * L.G 4 * (↑4! : ℂ) =
    0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
simp :
  (if x + (↑l : ℂ) ∈ L.lattice then 0
    else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃) =
    if x ∈ L.lattice then 0
    else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃
⊢ L.relation (x + (↑l : ℂ)) = L.relation x

Tactic:
simp only [relation, derivWeierstrassP_add_coe, weierstrassP_add_coe]

Premises used: PeriodPair.weierstrassP_add_coe, _private.0.PeriodPair.relation, PeriodPair.derivWeierstrassP_add_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
e_c : (x + (↑l : ℂ) ∈ L.lattice) = (x ∈ L.lattice)
⊢ (if x + (↑l : ℂ) ∈ L.lattice then 0
    else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃) =
    if x ∈ L.lattice then 0
    else HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ (x + (↑l : ℂ) ∈ L.lattice) = (x ∈ L.lattice)

Tactic:
simpa using (L.lattice.toAddSubgroup.add_mem_cancel_right (y := x) l.2)

Premises used: AddSubgroup.add_mem_cancel_right, Submodule.toAddSubgroup, PeriodPair.lattice, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
l : ↥L.lattice
rw : L.relation (x - (↑l : ℂ) + (↑l : ℂ)) = L.relation x
rw₁ rw₂ : L.relation x = L.relation x
⊢ L.relation (x - (↑l : ℂ)) = L.relation x

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

Premises used: _private.0.PeriodPair.relation_add_coe, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
pos : ∀ (hx : x ∈ L.lattice), AnalyticAt ℂ L.relation x
neg : ∀ (hx : x ∉ L.lattice), AnalyticAt ℂ L.relation x
⊢ AnalyticAt ℂ L.relation x

Tactic:
by_cases hx : x ∈ L.lattice

Premises used: PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ x ∈ L.lattice

Tactic:
hx
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
pos : ∀ (x : ↥L.lattice), AnalyticAt ℂ L.relation (↑x : ℂ)
⊢ AnalyticAt ℂ L.relation x

Tactic:
lift x to L.lattice using hx

Premises used: PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ↥L.lattice
⊢ AnalyticAt ℂ L.relation 0

Tactic:
have := L.analyticAt_relation_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation 0
⊢ AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))

Tactic:
rw [← sub_self x.1] at this

Premises used: sub_self, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))
⊢ AnalyticAt ℂ (F := ℂ) (fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)) (↑x : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))
h : L.relation = L.relation ∘ fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)
⊢ AnalyticAt ℂ L.relation (↑x : ℂ)

Tactic:
convert! this.comp (f := (· - x.1)) (by fun_prop)

Premises used: AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))
h : ∀ (a : ℂ), L.relation a = (L.relation ∘ fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)) a
⊢ L.relation = L.relation ∘ fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)

Tactic:
ext a
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))
a : ℂ
⊢ L.relation a = (L.relation ∘ fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)) a

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ ℘'[L] x

Tactic:
have := L.analyticOnNhd_derivWeierstrassP _ hx
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this : AnalyticAt ℂ ℘'[L] x
⊢ AnalyticAt ℂ ℘[L] x

Tactic:
have := L.analyticOnNhd_weierstrassP _ hx
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this_1 : AnalyticAt ℂ ℘'[L] x
this : AnalyticAt ℂ ℘[L] x
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x

Tactic:
have : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x := by
      have := L.analyticOnNhd_derivWeierstrassP _ hx
      have := L.analyticOnNhd_weierstrassP _ hx
      fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x
neg :
  (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝 x]
    L.relation
⊢ AnalyticAt ℂ L.relation x

Tactic:
apply this.congr

Premises used: AnalyticAt.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x
h :
  ∀ (x : ℂ) (hx : x ∈ (↑L.lattice : Set ℂ)ᶜ),
    HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃ = L.relation x
⊢ (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝 x]
    L.relation

Tactic:
filter_upwards [L.isClosed_lattice.isOpen_compl.mem_nhds hx] with x hx

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x_1 : ℂ
hx_1 : x_1 ∉ L.lattice
this :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x_1
x : ℂ
hx : x ∈ (↑L.lattice : Set ℂ)ᶜ
⊢ HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃ = L.relation x

Tactic:
simp_all [relation]

Premises used: _private.0.PeriodPair.relation
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
h : ∀ (x : ℂ), L.relation x = 0 x
⊢ L.relation = 0

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
⊢ Differentiable ℂ L.relation

Tactic:
have : Differentiable ℂ L.relation := fun x ↦ (L.analyticAt_relation x).differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z w : ℂ
hw : w ∈ L.lattice
⊢ w ∈ L.lattice

Tactic:
hw

Premises used: Set.Mem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z w : ℂ
hw : w ∈ L.lattice
lift : ∀ (w : ↥L.lattice), L.relation (z + (↑w : ℂ)) = L.relation z
⊢ L.relation (z + w) = L.relation z

Tactic:
lift w to L.lattice using hw

Premises used: PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z : ℂ
w : ↥L.lattice
⊢ L.relation (z + (↑w : ℂ)) = L.relation z

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
⊢ 0 ∈ L.lattice

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
⊢ L.relation x = 0 x

Tactic:
exact (this.apply_eq_apply_of_bounded (IsZLattice.isCompact_range_of_periodic L.lattice _
    this.continuous fun z w hw ↦ by lift w to L.lattice using hw; simp).isBounded x 0).trans
    (if_pos (by simp))

Premises used: IsCompact.isBounded, if_pos, Differentiable.apply_eq_apply_of_bounded, IsZLattice.isCompact_range_of_periodic, OfNat.ofNat, PeriodPair.lattice, Differentiable.continuous, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z : ℂ
hz : z ∉ L.lattice
⊢ HPow.hPow (β := ℕ) (℘'[L] z) 2 = 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 - L.g₂ * ℘[L] z - L.g₃

Tactic:
simpa [sub_eq_zero, relation, hz, sub_add] using congr($L.relation_eq_zero z)

Premises used: sub_add, sub_eq_zero, _private.0.PeriodPair.relation
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x z : ℂ
hz : ‖z‖ ≤ 1
e_a : cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
⊢ ‖cexp (x + z) - cexp x - z * cexp x‖ = ‖cexp x * (cexp z - 1 - z)‖

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x z : ℂ
hz : ‖z‖ ≤ 1
e_a : cexp x * cexp z - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
⊢ cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)

Tactic:
rw [exp_add]

Premises used: Complex.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp x * cexp z - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)

Tactic:
have hy_eq : y = x + (y - x) := by abel
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
rw : ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖
⊢ HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖

Tactic:
rw [pow_two]

Premises used: pow_two
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖

Tactic:
mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg

Premises used: le_rfl, LT.lt.le, mul_le_mul, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖

Tactic:
exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg

Premises used: le_rfl, LT.lt.le, mul_le_mul, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖

Tactic:
have hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖ := by
    rw [pow_two]
    exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x - z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖cexp (x + z) - cexp x - z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
rw : ‖cexp (x + z) - cexp x‖ - ‖z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
rw [← sub_le_iff_le_add', ← norm_smul z]

Premises used: norm_smul, sub_le_iff_le_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖cexp (x + z) - cexp x - z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ‖cexp (x + z) - cexp x‖ - ‖z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
(norm_sub_norm_le _ _).trans this

Premises used: norm_sub_norm_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖cexp (x + z) - cexp x - z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ‖cexp (x + z) - cexp x‖ - ‖z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
exact (norm_sub_norm_le _ _).trans this

Premises used: norm_sub_norm_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
⊢ ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
have h_sq : ∀ z, ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2 := by
    intro z hz
    have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
    rw [← sub_le_iff_le_add', ← norm_smul z]
    exact (norm_sub_norm_le _ _).trans this
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
nth_rw nth_rw₁ : ‖cexp (x + (y - x)) - cexp x‖ = ‖cexp (x + (y - x)) - cexp x‖
⊢ ‖cexp y - cexp x‖ = ‖cexp (x + (y - x)) - cexp x‖

Tactic:
nth_rw 1 [hy_eq]
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ‖cexp (x + (y - x)) - cexp x‖ ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖y - x‖ 2

Tactic:
h_sq (y - x) (hyx.le.trans hr_le)

Premises used: HSub.hSub, LT.lt.le, LE.le.trans