awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
succ :
  (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * L.sumInvPow l (n + 1 + 2) =
    (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)) * L.sumInvPow l (n + 1 + 2) /
      (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ))
⊢ (if n + 1 = 0 then ℘[L - l] l else HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1 * L.sumInvPow l (n + 1 + 2)) =
    (if n + 1 = 0 then ℘[L - l] l else (↑(n + 1 + 1)! : ℂ) * L.sumInvPow l (n + 1 + 2)) / (↑(n + 1)! : ℂ)

Tactic:
simp [Nat.factorial_succ]

Premises used: Nat.factorial_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * L.sumInvPow l (n + 1 + 2) =
    (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)) * L.sumInvPow l (n + 1 + 2) /
      (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ))

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
refine_1 : HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)
refine_2 : Metric.eball x (↑r : ENNReal) ⊆ Metric.closedBall x (↑r : ℝ)
⊢ HasFPowerSeriesOnBall ℘'[L - l₀] (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)

Tactic:
refine .congr ?_
    ((L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept l₀).mono (.trans ?_ hr))
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)

Tactic:
have := (L.hasFPowerSeriesOnBall_weierstrassPExcept l₀ x r hr0 hr).fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
⊢ HasFPowerSeriesOnBall (F := ℂ)
    (Function.comp (β := ℂ →L[ℂ] ℂ)
      (⇑((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1) : (a : ℂ →L[ℂ] ℂ) → ℂ) (fderiv ℂ ℘[L - l₀]))
    (ContinuousLinearMap.compFormalMultilinearSeries ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
      (L.weierstrassPExceptSeries l₀ x).derivSeries)
    x (↑r : ENNReal)

Tactic:
(ContinuousLinearMap.apply ℂ ℂ (1 : ℂ)).comp_hasFPowerSeriesOnBall this

Premises used: ContinuousLinearMap.apply, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
h :
  L.derivWeierstrassPExceptSeries l₀ x =
    ContinuousLinearMap.compFormalMultilinearSeries ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
      (L.weierstrassPExceptSeries l₀ x).derivSeries
⊢ HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x (↑r : ENNReal)

Tactic:
convert! (ContinuousLinearMap.apply ℂ ℂ (1 : ℂ)).comp_hasFPowerSeriesOnBall this

Premises used: ContinuousLinearMap.apply, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
h :
  ∀ (n : ℕ),
    Eq (α := ℂ) ((L.derivWeierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ 1 : ℂ)
      ((ContinuousLinearMap.compFormalMultilinearSeries
              ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
              (L.weierstrassPExceptSeries l₀ x).derivSeries n :
            (a : (i : Fin n) → ℂ) → ℂ)
          fun (x : Fin n) ↦ 1 :
        ℂ)
⊢ L.derivWeierstrassPExceptSeries l₀ x =
    ContinuousLinearMap.compFormalMultilinearSeries ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
      (L.weierstrassPExceptSeries l₀ x).derivSeries

Tactic:
ext n
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
n : ℕ
h :
  HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 *
      (L.sumInvPow x (n + 3) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 3))⁻¹ else 0) =
    HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 *
      ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) *
        (L.sumInvPow x (n + 1 + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 1 + 2))⁻¹ else 0))
⊢ Eq (α := ℂ) ((L.derivWeierstrassPExceptSeries l₀ x n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ 1 : ℂ)
    ((ContinuousLinearMap.compFormalMultilinearSeries
            ((ContinuousLinearMap.apply ℂ ℂ : (a : ℂ) → (ℂ →L[ℂ] ℂ) →L[ℂ] ℂ) 1)
            (L.weierstrassPExceptSeries l₀ x).derivSeries n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)

Tactic:
simp [weierstrassPExceptSeries, derivWeierstrassPExceptSeries]

Premises used: PeriodPair.weierstrassPExceptSeries, PeriodPair.derivWeierstrassPExceptSeries
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x (↑r : ENNReal)
n : ℕ
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 *
      (L.sumInvPow x (n + 3) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 3))⁻¹ else 0) =
    HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 *
      ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) *
        (L.sumInvPow x (n + 1 + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 1 + 2))⁻¹ else 0))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ
⊢ Metric.eball x (↑r : ENNReal) ⊆ Metric.closedBall x (↑r : ℝ)

Tactic:
simpa using Metric.ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
obtain :
  ∀ (r : ℝ) (h₁ : 0 < r) (h₂ : Metric.closedBall l r ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ),
    HasFPowerSeriesAt (𝕜 := ℂ) ℘'[L - l]
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * L.sumInvPow l (i + 3))
      l
⊢ HasFPowerSeriesAt (𝕜 := ℂ) ℘'[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * L.sumInvPow l (i + 3))
    l

Tactic:
obtain ⟨r, h₁, h₂⟩ := Metric.nhds_basis_closedBall.mem_iff.mp
    (L.compl_lattice_diff_singleton_mem_nhds l)

Premises used: Filter.HasBasis.mem_iff, PeriodPair.compl_lattice_diff_singleton_mem_nhds, Iff.mp, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ ((↑L.lattice : Set ℂ) \ {l})ᶜ
⊢ HasFPowerSeriesAt (𝕜 := ℂ) ℘'[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑i : ℂ) 2 * L.sumInvPow l (i + 3))
    l

Tactic:
simpa [derivWeierstrassPExceptSeries] using
    (L.hasFPowerSeriesOnBall_derivWeierstrassPExcept l l ⟨r, h₁.le⟩ h₁ h₂).hasFPowerSeriesAt

Premises used: LT.lt.le, Subtype.mk, PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept, PeriodPair.derivWeierstrassPExceptSeries, HasFPowerSeriesOnBall.hasFPowerSeriesAt
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
⊢ AnalyticOnNhd ℂ ℘'[L - l₀] ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
(L.differentiableOn_derivWeierstrassPExcept l₀).analyticOnNhd L.isOpen_compl_lattice_diff

Premises used: PeriodPair.isOpen_compl_lattice_diff, DifferentiableOn.analyticOnNhd, PeriodPair.differentiableOn_derivWeierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘'[L - l] l / (↑n ! : ℂ) =
    HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3)

Tactic:
simpa using congr($((L.analyticAt_derivWeierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_derivWeierstrassPExcept l)).coeff n)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘'[L - l] l / (↑n ! : ℂ) =
    HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3)

Tactic:
have : iteratedDeriv n ℘'[L - l] l / n ! = (↑n + 1) * (↑n + 2) * L.sumInvPow l (n + 3) := by
    simpa using congr($((L.analyticAt_derivWeierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_derivWeierstrassPExcept l)).coeff n)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
this :
  iteratedDeriv n ℘'[L - l] l / (↑n ! : ℂ) =
    HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3)
simp :
  ∀
    (this :
      iteratedDeriv n ℘'[L - l] l =
        HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3) * (↑n ! : ℂ)),
    iteratedDeriv n ℘'[L - l] l =
      (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)) * L.sumInvPow l (n + 3)
⊢ iteratedDeriv n ℘'[L - l] l = (↑(n + 2)! : ℂ) * L.sumInvPow l (n + 3)

Tactic:
simp [div_eq_iff, Nat.factorial_ne_zero, Nat.factorial_succ] at this ⊢

Premises used: Nat.factorial_succ, div_eq_iff, Nat.factorial_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
n : ℕ
this :
  iteratedDeriv n ℘'[L - l] l =
    HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * L.sumInvPow l (n + 3) * (↑n ! : ℂ)
⊢ iteratedDeriv n ℘'[L - l] l =
    (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)) * L.sumInvPow l (n + 3)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l : ℂ
⊢ deriv ℘'[L - l] l = 6 * L.sumInvPow l 4

Tactic:
simpa using L.iteratedDeriv_derivWeierstrassPExcept_self l (n := 1)

Premises used: PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ AnalyticOnNhd ℂ ℘'[L] (↑L.lattice : Set ℂ)ᶜ

Tactic:
L.differentiableOn_derivWeierstrassP.analyticOnNhd L.isClosed_lattice.isOpen_compl

Premises used: IsClosed.isOpen_compl, PeriodPair.differentiableOn_derivWeierstrassP, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
h : ∀ (z : ℂ) (i : ℕ) (f : i = 0), ℘[L - l₀] = ℘[L]
h₁ :
  ∀ (z : ℂ) (i : ℕ),
    ¬i = 0 → (L.sumInvPow z (i + 2) - if l₀ ∈ L.lattice then ((l₀ - z) ^ (i + 2))⁻¹ else 0) = L.sumInvPow z (i + 2)
⊢ Eq (α := (x : ℂ) → FormalMultilinearSeries ℂ ℂ ℂ)
    (fun (x : ℂ) ↦
      FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x
        else
          HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 *
            (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0))
    fun (x : ℂ) ↦
    FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      if i = 0 then ℘[L] x else HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * L.sumInvPow x (i + 2)

Tactic:
congr! with z i f
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
z : ℂ
i : ℕ
f : i = 0
h h₁ : ℘[L] = ℘[L]
⊢ ℘[L - l₀] = ℘[L]

Tactic:
rw [L.weierstrassPExcept_of_notMem _ hl₀]

Premises used: PeriodPair.weierstrassPExcept_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
z : ℂ
i : ℕ
h : ¬i = 0
⊢ (L.sumInvPow z (i + 2) - if l₀ ∈ L.lattice then ((l₀ - z) ^ (i + 2))⁻¹ else 0) = L.sumInvPow z (i + 2)

Tactic:
simp [hl₀]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
⊢ L.weierstrassPExceptSummand l₀ = L.weierstrassPSummand

Tactic:
grind [weierstrassPSummand, weierstrassPExceptSummand]

Premises used: PeriodPair.weierstrassPExceptSummand, PeriodPair.weierstrassPSummand
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
i : ℕ
simp_rw : (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
simp_rw₁ :
  Eq (α := ℂ) (∑' (l : ↥L.lattice), L.weierstrassPExceptSummand (L.ω₁ / 2) x i l)
    (∑' (l : ↥L.lattice), L.weierstrassPSummand x i l)
⊢ (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l

Tactic:
simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    L.coeff_weierstrassPExceptSeries,
    ← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]

Premises used: PeriodPair.coeff_weierstrassPExceptSeries, PeriodPair.ω₁_div_two_notMem_lattice, PeriodPair.weierstrassPExceptSummand_of_notMem, PeriodPair.weierstrassPExceptSeries_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
simp_rw :
  Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand (L.ω₁ / 2) x b c * (z - x) ^ b)
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPSummand x b c * (z - x) ^ b)

Tactic:
simp_rw [← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, PeriodPair.weierstrassPExceptSummand_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand (L.ω₁ / 2) x b c * (z - x) ^ b)

Tactic:
L.summable_weierstrassPExceptSummand _ z x fun l hl ↦ hx l

Premises used: PeriodPair.summable_weierstrassPExceptSummand
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand (L.ω₁ / 2) x b c * (z - x) ^ b)

Tactic:
refine L.summable_weierstrassPExceptSummand _ z x fun l hl ↦ hx l

Premises used: PeriodPair.summable_weierstrassPExceptSummand
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
simp_rw : HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L - L.ω₁ / 2] z)
⊢ HasSum (fun (i : ℕ) ↦ (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (℘[L] z)

Tactic:
simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, PeriodPair.weierstrassPExceptSeries_of_notMem, PeriodPair.weierstrassPExcept_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L - L.ω₁ / 2] z)

Tactic:
L.weierstrassPExceptSeries_hasSum _ z x fun l hl ↦ hx l

Premises used: PeriodPair.weierstrassPExceptSeries_hasSum
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖(↑l : ℂ) - x‖
⊢ HasSum (fun (i : ℕ) ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L - L.ω₁ / 2] z)

Tactic:
exact L.weierstrassPExceptSeries_hasSum _ z x fun l hl ↦ hx l

Premises used: PeriodPair.weierstrassPExceptSeries_hasSum
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ (↑L.lattice : Set ℂ)ᶜ
simp_rw : HasFPowerSeriesOnBall ℘[L - L.ω₁ / 2] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x (↑r : ENNReal)
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPSeries x) x (↑r : ENNReal)

Tactic:
simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

Premises used: PeriodPair.ω₁_div_two_notMem_lattice, PeriodPair.weierstrassPExceptSeries_of_notMem, PeriodPair.weierstrassPExcept_of_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ (↑L.lattice : Set ℂ)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - L.ω₁ / 2] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x (↑r : ENNReal)

Tactic:
L.hasFPowerSeriesOnBall_weierstrassPExcept _ x r hr0
    (hr.trans (Set.compl_subset_compl.mpr Set.diff_subset))

Premises used: Iff.mpr, Set.diff_subset, HasSubset.Subset.trans, Set.compl_subset_compl, PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x (↑r : ℝ) ⊆ (↑L.lattice : Set ℂ)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - L.ω₁ / 2] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x (↑r : ENNReal)

Tactic:
exact L.hasFPowerSeriesOnBall_weierstrassPExcept _ x r hr0
    (hr.trans (Set.compl_subset_compl.mpr Set.diff_subset))

Premises used: Iff.mpr, Set.diff_subset, HasSubset.Subset.trans, Set.compl_subset_compl, PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ AnalyticOnNhd ℂ ℘[L] (↑L.lattice : Set ℂ)ᶜ

Tactic:
L.differentiableOn_weierstrassP.analyticOnNhd L.isClosed_lattice.isOpen_compl

Premises used: IsClosed.isOpen_compl, DifferentiableOn.analyticOnNhd, PeriodPair.differentiableOn_weierstrassP
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
z : ℂ
⊢ (if z = l₀ then 1 else HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L] z) =
    HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2

Tactic:
grind [L.weierstrassPExcept_add ⟨_, hl₀⟩]

Premises used: Subtype.mk, PeriodPair.weierstrassPExcept_add
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
pos : ∀ (hx : x ∈ L.lattice), MeromorphicAt ℘[L] x
neg : ∀ (hx : x ∉ L.lattice), MeromorphicAt ℘[L] x
⊢ MeromorphicAt ℘[L] 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
pos :
  MeromorphicAt (E := ℂ)
    (fun (x_1 : ℂ) ↦ ℘[L - x] x_1 + (1 / HPow.hPow (β := ℕ) (x_1 - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x
⊢ MeromorphicAt ℘[L] x

Tactic:
simp_rw [← funext <| L.weierstrassPExcept_add ⟨x, hx⟩]

Premises used: Subtype.mk, funext, PeriodPair.weierstrassPExcept_add
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ x ∈ ((↑L.lattice : Set ℂ) \ {x})ᶜ

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

Tactic:
have := (analyticOnNhd_weierstrassPExcept L x x (by simp)).meromorphicAt
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
this : MeromorphicAt ℘[L - x] x
⊢ MeromorphicAt (E := ℂ)
    (fun (x_1 : ℂ) ↦ ℘[L - x] x_1 + (1 / HPow.hPow (β := ℕ) (x_1 - x) 2 - 1 / HPow.hPow (β := ℕ) x 2)) x

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

Tactic:
(L.analyticOnNhd_weierstrassP x hx).meromorphicAt

Premises used: PeriodPair.analyticOnNhd_weierstrassP, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ MeromorphicAt ℘[L] x

Tactic:
exact (L.analyticOnNhd_weierstrassP x hx).meromorphicAt

Premises used: PeriodPair.analyticOnNhd_weierstrassP, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
rw : Meromorphic (deriv ℘[L])
⊢ Meromorphic ℘'[L]

Tactic:
rw [← deriv_weierstrassP]

Premises used: PeriodPair.deriv_weierstrassP
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Meromorphic (deriv ℘[L])

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
trans : meromorphicOrderAt ℘[L] l₀ = (↑(-2) : WithTop ℤ)
trans₁ : Eq (α := WithTop ℤ) (↑(-2) : WithTop ℤ) (-2)
⊢ meromorphicOrderAt ℘[L] l₀ = -2

Tactic:
trans ↑(-2 : ℤ)

Premises used: OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
rw :
  ∃ (g : ℂ → ℂ), AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = HPow.hPow (β := ℤ) (z - l₀) (-2) • g z
⊢ meromorphicOrderAt ℘[L] l₀ = (↑(-2) : WithTop ℤ)

Tactic:
rw [meromorphicOrderAt_eq_int_iff (L.meromorphic_weierstrassP l₀)]

Premises used: meromorphicOrderAt_eq_int_iff, PeriodPair.meromorphic_weierstrassP
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = HPow.hPow (β := ℤ) (z - l₀) (-2) • g z

Tactic:
⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, PeriodPair.weierstrassPExcept
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
refine_1 :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
    l₀
refine_2 :
  Ne (α := ℂ)
    ((fun (z : ℂ) ↦
        HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
      l₀)
    0
refine_3 :
  ∀ᶠ (z : ℂ) in 𝓝[≠] l₀,
    ℘[L] z =
      HSMul.hSMul (β := ℂ) (HPow.hPow (β := ℤ) (z - l₀) (-2))
        ((fun (z : ℂ) ↦
            HPow.hPow (β := ℕ) (z - l₀) 2 * ℘[L - l₀] z + 1 - HPow.hPow (β := ℕ) (z - l₀) 2 / HPow.hPow (β := ℕ) l₀ 2)
          z)
⊢ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = HPow.hPow (β := ℤ) (z - l₀) (-2) • g z

Tactic:
refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ l₀ ∈ ((↑L.lattice : Set ℂ) \ {l₀})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ AnalyticAt ℂ ℘[L - l₀] l₀

Tactic:
have : AnalyticAt ℂ ℘[L - l₀] l₀ := L.analyticOnNhd_weierstrassPExcept l₀ l₀ (by simp)