awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
obtain :
  ∀ (κ : ℝ) (hκ : κ > 0)
    (hκ' :
      Subset (α := Set ℝ) (Metric.ball 1 κ)
        ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)),
    ∃ (κ : ℝ), 1 < κ ∧ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
⊢ ∃ (κ : ℝ), 1 < κ ∧ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖

Tactic:
obtain ⟨κ, hκ, hκ'⟩ := Metric.isOpen_iff.mp ((continuous_mul_const ‖z - x‖).isOpen_preimage _
      (isClosedMap_dist x _
      (L.isClosed_of_subset_lattice (Set.diff_subset (t := {l₀})))).upperClosure.isOpen_compl) 1
      (by simpa [Complex.dist_eq, @forall_comm ℝ, norm_sub_rev x] using hx)

Premises used: Norm.norm, IsClosed.isOpen_compl, HSub.hSub, Metric.isOpen_iff, Iff.mp, OfNat.ofNat, Continuous.isOpen_preimage, continuous_mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
⊢ 1 < κ / 2 + 1

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
refine : ∀ (l : ↥L.lattice) (hl : (↑l : ℂ) ≠ l₀), ‖z - x‖ * (κ / 2 + 1) < ‖(↑l : ℂ) - x‖
⊢ ∃ (κ : ℝ), 1 < κ ∧ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖

Tactic:
refine ⟨κ / 2 + 1, by simpa, fun l hl ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
l : ↥L.lattice
hl : (↑l : ℂ) ≠ l₀
⊢ Membership.mem (γ := Set ℝ) (Metric.ball 1 κ) (κ / 2 + 1)

Tactic:
simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ]

Premises used: Iff.mpr, LT.lt.le, div_lt_iff₀, abs_eq_self
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
l : ↥L.lattice
hl : (↑l : ℂ) ≠ l₀
⊢ ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l

Tactic:
simpa using @hκ' (κ / 2 + 1) (by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ])
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
l : ↥L.lattice
hl : (↑l : ℂ) ≠ l₀
⊢ ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l

Tactic:
have : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l := by
      simpa using @hκ' (κ / 2 + 1) (by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ])
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : κ > 0
hκ' :
  Subset (α := Set ℝ) (Metric.ball 1 κ)
    ((fun (x_1 : ℝ) ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' ((↑L.lattice : Set ℂ) \ {l₀}))) : Set ℝ)ᶜ)
l : ↥L.lattice
hl : (↑l : ℂ) ≠ l₀
this : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l
⊢ ‖z - x‖ * (κ / 2 + 1) < ‖(↑l : ℂ) - x‖

Tactic:
simpa only [Complex.dist_eq, norm_sub_rev x, mul_comm] using this _ l.2 hl

Premises used: Complex.dist_eq, mul_comm, norm_sub_rev, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
obtain :
  ∀ (κ : ℝ) (hκ : 1 < κ) (hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖),
    Summable (α := ℂ) (β := ℕ × ↥L.lattice)
      (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

Tactic:
obtain ⟨κ, hκ, hκ'⟩ : ∃ κ : ℝ, 1 < κ ∧ ∀ l : L.lattice, l.1 ≠ l₀ → ‖z - x‖ * κ < ‖l - x‖ := by
    obtain ⟨κ, hκ, hκ'⟩ := Metric.isOpen_iff.mp ((continuous_mul_const ‖z - x‖).isOpen_preimage _
      (isClosedMap_dist x _
      (L.isClosed_of_subset_lattice (Set.diff_subset (t := {l₀})))).upperClosure.isOpen_compl) 1
      (by simpa [Complex.dist_eq, @forall_comm ℝ, norm_sub_rev x] using hx)
    refine ⟨κ / 2 + 1, by simpa, fun l hl ↦ ?_⟩
    have : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l := by
      simpa using @hκ' (κ / 2 + 1) (by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ])
    simpa only [Complex.dist_eq, norm_sub_rev x, mul_comm] using this _ l.2 hl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
rw :
  Summable (α := ℂ) (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
    (Function.comp (β := ℕ × ↥L.lattice)
      (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
      (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

Tactic:
rw [← e.symm.summable_iff]

Premises used: Equiv.summable_iff, Equiv.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
h₁ :
  Summable (α := ℂ) (β := ↥L.lattice)
    (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
      (Function.comp (β := ℕ × ↥L.lattice)
        (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
        (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
      Sum.inl)
h₂ :
  Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
      (Function.comp (β := ℕ × ↥L.lattice)
        (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
        (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
      Sum.inr)
⊢ Summable (α := ℂ) (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
    (Function.comp (β := ℕ × ↥L.lattice)
      (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
      (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))

Tactic:
apply Summable.sum

Premises used: Summable.sum
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ Summable (α := ℂ) (β := ↥L.lattice)
    (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
      (Function.comp (β := ℕ × ↥L.lattice)
        (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
        (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
      Sum.inl)

Tactic:
simpa [weierstrassPExceptSummand, e, Function.comp_def, Function.uncurry, sub_sq_comm x,
      Denumerable.eqv] using (L.hasSum_weierstrassPExcept l₀ x).summable

Premises used: Denumerable.eqv, PeriodPair.weierstrassPExceptSummand, sub_sq_comm, HasSum.summable, Function.comp_def, PeriodPair.hasSum_weierstrassPExcept, Function.uncurry
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
h₂ :
  Summable (α := ℂ) fun (x_1 : ℕ × ↥L.lattice) ↦
    (if (↑x_1.2 : ℂ) = l₀ then 0
      else
        HAdd.hAdd (α := ℂ) (↑(x_1.1 + 1) : ℂ) 1 * ((↑x_1.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑x_1.1 : ℤ) 1 + 2)) - 0) *
      (z - x) ^ (x_1.1 + 1)
⊢ Summable (α := ℂ) (β := ℕ × ↥L.lattice)
    (Function.comp (β := ↥L.lattice ⊕ ℕ × ↥L.lattice)
      (Function.comp (β := ℕ × ↥L.lattice)
        (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
        (⇑e.symm : (a : ↥L.lattice ⊕ ℕ × ↥L.lattice) → ℕ × ↥L.lattice))
      Sum.inr)

Tactic:
dsimp [e, Function.comp_def, Function.uncurry_def, Denumerable.eqv, weierstrassPExceptSummand]

Premises used: Denumerable.eqv, Function.uncurry_def, PeriodPair.weierstrassPExceptSummand, Function.comp_def
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ |κ⁻¹| < 1

Tactic:
grind [abs_inv, inv_lt_one_iff₀]

Premises used: abs_inv, inv_lt_one_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ |κ⁻¹| < 1

Tactic:
have : |κ⁻¹| < 1 := by grind [abs_inv, inv_lt_one_iff₀]
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
this : |κ⁻¹| < 1
⊢ Membership.mem (γ := Set ℝ) (Metric.eball 0 1) κ⁻¹

Tactic:
simpa [enorm_eq_nnnorm]

Premises used: enorm_eq_nnnorm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
this : |κ⁻¹| < 1
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))

Tactic:
simpa [mul_comm] using ((Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero 1 2).hasSum
        (y := κ⁻¹) (by simpa [enorm_eq_nnnorm])).summable

Premises used: Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero, HasFPowerSeriesOnBall.hasSum, HasSum.summable, mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))

Tactic:
have H₁ : Summable fun i : ℕ ↦ ((i + 2) * κ ^ (-i : ℤ)) := by
      have : |κ⁻¹| < 1 := by grind [abs_inv, inv_lt_one_iff₀]
      simpa [mul_comm] using ((Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero 1 2).hasSum
        (y := κ⁻¹) (by simpa [enorm_eq_nnnorm])).summable
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
⊢ LT.lt (α := ℤ) (-3) (-(↑(finrank ℤ ↥L.lattice) : ℤ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
⊢ Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖

Tactic:
have H₂ : Summable fun l : L.lattice ↦ ‖l - x‖ ^ (-3 : ℤ) * ‖z - x‖ :=
      (ZLattice.summable_norm_sub_zpow _ _ (by simp) _).mul_right _
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
i : ℕ
⊢ LE.le (α := (fun (a : ℕ) ↦ ℝ) i) (0 i)
    ((fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))) i)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
i : ↥L.lattice
⊢ LE.le (α := (fun (a : ↥L.lattice) ↦ ℝ) i) (0 i)
    ((fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖) i)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
h₂ :
  ∀ (i : ℕ × ↥L.lattice),
    ‖(if (↑i.2 : ℂ) = l₀ then 0
          else
            HAdd.hAdd (α := ℂ) (↑(i.1 + 1) : ℂ) 1 * ((↑i.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑i.1 : ℤ) 1 + 2)) - 0) *
          (z - x) ^ (i.1 + 1)‖ ≤
      HAdd.hAdd (α := ℝ) (↑i.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i.1 : ℤ)) *
        (HPow.hPow (β := ℤ) ‖(↑i.2 : ℂ) - x‖ (-3) * ‖z - x‖)
⊢ Summable (α := ℂ) fun (x_1 : ℕ × ↥L.lattice) ↦
    (if (↑x_1.2 : ℂ) = l₀ then 0
      else
        HAdd.hAdd (α := ℂ) (↑(x_1.1 + 1) : ℂ) 1 * ((↑x_1.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑x_1.1 : ℤ) 1 + 2)) - 0) *
      (z - x) ^ (x_1.1 + 1)

Tactic:
refine (H₁.mul_of_nonneg H₂ (by intro; positivity) (by intro; positivity)).of_norm_bounded ?_

Premises used: Summable.mul_of_nonneg, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
pos :
  ∀ (hp : (↑p.2 : ℂ) = l₀),
    ‖0 * (z - x) ^ (p.1 + 1)‖ ≤
      HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
        (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
neg :
  ∀ (hp : ¬(↑p.2 : ℂ) = l₀),
    ‖(HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
          (z - x) ^ (p.1 + 1)‖ ≤
      HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
        (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)
⊢ ‖(if (↑p.2 : ℂ) = l₀ then 0
        else HAdd.hAdd (α := ℂ) (↑(p.1 + 1) : ℂ) 1 * ((↑p.2 : ℂ) - x) ^ (-(HAdd.hAdd (α := ℤ) (↑p.1 : ℤ) 1 + 2)) - 0) *
        (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)

Tactic:
split_ifs with hp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : (↑p.2 : ℂ) = l₀
pos : 0 ≤ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * (κ ^ p.1)⁻¹ * ((HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)
⊢ ‖0 * (z - x) ^ (p.1 + 1)‖ ≤
    HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑p.1 : ℤ)) *
      (HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ (-3) * ‖z - x‖)

Tactic:
simp only [zero_mul, norm_zero, zpow_neg, zpow_natCast, Int.reduceNeg]

Premises used: zpow_natCast, Int.reduceNeg, MulZeroClass.zero_mul, norm_zero, zpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : (↑p.2 : ℂ) = l₀
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑p.1 : ℝ) 2 * (κ ^ p.1)⁻¹ * ((HPow.hPow (β := ℤ) ‖(↑p.2 : ℂ) - x‖ 3)⁻¹ * ‖z - x‖)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
h : ‖(↑p.2 : ℂ) - x‖ = 0
⊢ (↑p.2 : ℂ) = x

Tactic:
simpa [sub_eq_zero] using h

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
h : ‖(↑p.2 : ℂ) - x‖ = 0
⊢ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖

Tactic:
obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h

Premises used: Prod.snd, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ < ‖(↑l : ℂ) - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - x‖ * κ < ‖(↑l : ℂ) - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  Equiv.trans (Equiv.prodCongrLeft fun (x : ↥L.lattice) ↦ Equiv.symm (Denumerable.eqv (Option ℕ))) optionProdEquiv
H₁ : Summable (α := ℝ) fun (i : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 2 * HPow.hPow (β := ℤ) κ (-(↑i : ℤ))
H₂ : Summable (α := ℝ) fun (l : ↥L.lattice) ↦ HPow.hPow (β := ℤ) ‖(↑l : ℂ) - x‖ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp : ¬(↑p.2 : ℂ) = l₀
h : ‖(↑p.2 : ℂ) - x‖ = 0
hx₁ : ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖
⊢ ∀ (l : ↥L.lattice), (↑l : ℂ) ≠ l₀ → ‖z - (↑p.2 : ℂ)‖ * κ < ‖(↑l : ℂ) - (↑p.2 : ℂ)‖

Tactic:
obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h

Premises used: Prod.snd, rfl