mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (∑ x ∈ s, if ↑x = l₀ then 0 else -2 / (l - ↑x) ^ 3) =
    ∑ i ∈ s, deriv (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l

pp: case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ i ∈ s, DifferentiableAt ℂ (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l

Tactic:
]

Goal state after:
case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (∑ x ∈ s, if ↑x = l₀ then 0 else -2 / (l - ↑x) ^ 3) =
    ∑ i ∈ s, deriv (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l

case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ i ∈ s, DifferentiableAt ℂ (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)

Tactic:
]

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2) l - 0

Tactic:
]

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2) l - 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ ↑n ^ (-(↑b.card + 1 - ↑a.card)) = ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
]

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ ↑n ^ (-(↑b.card + 1 - ↑a.card)) = ↑n ^ (↑a.card - ↑b.card - 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = ↑(-2) * (l - ↑x) ^ (-2 - 1) - 0

Tactic:
]

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = ↑(-2) * (l - ↑x) ^ (-2 - 1) - 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
h₁ : Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
this :
  Tendsto
    (fun x ↦
      ‖↑x ^ (↑a.card - ↑b.card - 1) *
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
            ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹)))‖)
    atTop (𝓝 0)
h_ne : ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0
n : ℕ
hn₁ : regularizedHGFunCoeff a b n ≠ 0
hn₂ : n ≠ 0
⊢ ‖↑n ^ (↑a.card - ↑b.card - 1) * (Multiset.map (fun x ↦ x / ↑n + 1) a).prod /
        ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹))‖ =
    ‖↑n ^ (↑a.card - ↑b.card - 1) * (Multiset.map (fun x ↦ x / ↑n + 1) a).prod /
        ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹))‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case neg
a b : Multiset ℂ
h : a.card = b.card + 1
j : ℂ
hj : j ∈ a
k : ℕ
h' : j = -↑k
⊢ 1 ≤ ⊤

Tactic:
]

Goal state after:
case neg
a b : Multiset ℂ
h : a.card = b.card + 1
j : ℂ
hj : j ∈ a
k : ℕ
h' : j = -↑k
⊢ 1 ≤ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
⊢ (∑' (c : ↥L.lattice), if ↑((Equiv.neg ↥L.lattice) c) = l₀ then 0 else -2 / (-z - ↑((Equiv.neg ↥L.lattice) c)) ^ 3) =
    -∑' (l : ↥L.lattice), if ↑l = -l₀ then 0 else -2 / (z - ↑l) ^ 3

Tactic:
]

Goal state after:
L : PeriodPair
l₀ z : ℂ
⊢ (∑' (c : ↥L.lattice), if ↑((Equiv.neg ↥L.lattice) c) = l₀ then 0 else -2 / (-z - ↑((Equiv.neg ↥L.lattice) c)) ^ 3) =
    -∑' (l : ↥L.lattice), if ↑l = -l₀ then 0 else -2 / (z - ↑l) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: ⊢ regularizedHGFun 0 0 = (NormedSpace.expSeries ℂ ℂ).sum

Tactic:
]

Goal state after:
⊢ regularizedHGFun 0 0 = (NormedSpace.expSeries ℂ ℂ).sum
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c : ℂ
⊢ regularizedHGFunSeries {b, a} {c} = regularizedHGFunSeries {b, a} {c}

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c : ℂ
⊢ (fun z ↦ (b.regularizedGaussHGFunSeries a c).sum z) = fun z ↦ (b.regularizedGaussHGFunSeries a c).sum z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ (∑' (c : ↥L.lattice), if ↑((Equiv.addRight l) c) = l₀ then 0 else -2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3) =
    ∑' (l_1 : ↥L.lattice), if ↑l_1 = l₀ - ↑l then 0 else -2 / (z - ↑l_1) ^ 3

Tactic:
]

Goal state after:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ (∑' (c : ↥L.lattice), if ↑((Equiv.addRight l) c) = l₀ then 0 else -2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3) =
    ∑' (l_1 : ↥L.lattice), if ↑l_1 = l₀ - ↑l then 0 else -2 / (z - ↑l_1) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ (Gamma c)⁻¹ *
      ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) *
        (Gamma (c + ↑n) / Gamma c)⁻¹) =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n ! * Gamma (c + ↑n))

Tactic:
]

Goal state after:
a b c : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ (Gamma c)⁻¹ *
      ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) *
        (Gamma (c + ↑n) / Gamma c)⁻¹) =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n ! * Gamma (c + ↑n))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
⊢ ((Gamma c)⁻¹ • ordinaryHypergeometricSeries ℂ a b c).sum z = (a.regularizedGaussHGFunSeries b c).sum z

Tactic:
]

Goal state after:
a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
⊢ ((Gamma c)⁻¹ • ordinaryHypergeometricSeries ℂ a b c).sum z = (a.regularizedGaussHGFunSeries b c).sum z
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ Integrable ((ball 0 r).indicator fun x ↦ f ‖x‖) μ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ Integrable ((ball 0 r).indicator fun x ↦ f ‖x‖) μ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬univ.Countable

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬univ.Countable
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ (1 + rexp (-x))⁻¹ * rexp (-x) = 1 - (1 + rexp (-x))⁻¹

Tactic:
]

Goal state after:
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * rexp (-x) = 1 - (1 + rexp (-x))⁻¹
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn ?m.237 (Ioi 0) volume ↔ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ ℝ → F

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ EqOn (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) ?m.237 (Ioi 0)

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ EqOn (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0)
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < x ∧ x < 1

Tactic:
]

Goal state after:
x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < x ∧ x < 1
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: case e'_9
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * ((1 + rexp (-x))⁻¹ * rexp (-x)) = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2

Tactic:
]

Goal state after:
case e'_9
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * ((1 + rexp (-x))⁻¹ * rexp (-x)) = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: ⊢ Subtype.val ⁻¹' Ioo 0 1 = Ioo 0 1

Tactic:
]

Goal state after:
⊢ Subtype.val ⁻¹' Ioo 0 1 = Ioo 0 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ ℘'[L - l₀ - ↑l] x = ℘'[L - l₀ - ↑l] x

pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ

Tactic:
]

Goal state after:
case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume ↔
    Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ support ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) ⊆ Ioi 0

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ support ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) ⊆ Ioi 0
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) univ volume ↔
    IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) univ volume

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L] (-(↑l / 2) + ↑l) + (1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2) =
    ℘[L] (↑l / 2) + (1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2 + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))

Tactic:
]

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L] (-(↑l / 2) + ↑l) + (1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2) =
    ℘[L] (↑l / 2) + (1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2 + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ ∫ (x : E), f ‖x‖ ∂μ = ∫ (x : E), f ‖x‖ ∂μ

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2) +
      (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) =
    ℘[L - ↑⟨z, hz⟩] z + (1 / (z - ↑⟨z, hz⟩) ^ 2 - 1 / ↑⟨z, hz⟩ ^ 2)

Tactic:
]

Goal state after:
case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2) +
      (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) =
    ℘[L - ↑⟨z, hz⟩] z + (1 / (z - ↑⟨z, hz⟩) ^ 2 - 1 / ↑⟨z, hz⟩ ^ 2)
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ dim E • μ.real (ball 0 1) • ∫ (x : ℝ) in Ioi 0, ?m.337 x ∂volume =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ ℝ → F

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : x ∈ Ioi 0
⊢ (x ^ (dim E - 1)).toNNReal • f x = ?m.337 x

pp: case f_meas
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : x ∈ Ioi 0
⊢ (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x

case f_meas
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (dim E - 1) • f x = x ^ (dim E - 1) • f x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - -↑l] z + -(↑l ^ 2)⁻¹ + (1 / (z + ↑l - 0) ^ 2 - 1 / 0 ^ 2) =
    ℘[L - ↑(-l)] z + (1 / (z - ↑(-l)) ^ 2 - 1 / ↑(-l) ^ 2)

Tactic:
]

Goal state after:
case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - -↑l] z + -(↑l ^ 2)⁻¹ + (1 / (z + ↑l - 0) ^ 2 - 1 / 0 ^ 2) =
    ℘[L - ↑(-l)] z + (1 / (z - ↑(-l)) ^ 2 - 1 / ↑(-l) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cos θ) (T ℂ n) = cos (↑n * θ)

Tactic:
induction n using Polynomial.Chebyshev.induct with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ {L.ω₁, L.ω₂} ⊆ ↑(AddSubgroup.toIntSubmodule G)

Tactic:
]

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ {L.ω₁, L.ω₂} ⊆ ↑(AddSubgroup.toIntSubmodule G)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cos θ) (U ℂ n) * sin θ = sin ((↑n + 1) * θ)

Tactic:
induction n using Polynomial.Chebyshev.induct with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cosh θ) (T ℂ n) = eval (cosh θ) (T ℂ n)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ↥L.lattice
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ cos (↑n * (θ * I)) = cos (↑n * (θ * I))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘[L] z = ℘[L] z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ sin ((↑n + 1) * (θ * I)) * -I = sin ((↑n + 1) * (θ * I)) * -I

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ((∑' (l : ↥L.lattice), if ↑l = ↑l₀ then 0 else -2 / (z - ↑l) ^ 3) +
      ∑' (i : ↥L.lattice), if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) =
    -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

Tactic:
← Summable.tsum_add,

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ∑' (b : ↥L.lattice), ((if ↑b = ↑l₀ then 0 else -2 / (z - ↑b) ^ 3) + if ↑b = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) =
    -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

case hf
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun l ↦ if ↑l = ↑l₀ then 0 else -2 / (z - ↑l) ^ 3

case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) = sinh ((↑n + 1) * θ)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ∑' (b : ↥L.lattice), ((if ↑b = ↑l₀ then 0 else -2 / (z - ↑b) ^ 3) + if ↑b = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) =
    ∑' (b : ↥L.lattice), -(2 / (z - ↑b) ^ 3)

pp: case hf
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun l ↦ if ↑l = ↑l₀ then 0 else -2 / (z - ↑l) ^ 3

pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0

Tactic:
]

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ∑' (b : ↥L.lattice), ((if ↑b = ↑l₀ then 0 else -2 / (z - ↑b) ^ 3) + if ↑b = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) =
    ∑' (b : ↥L.lattice), -(2 / (z - ↑b) ^ 3)

case hf
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun l ↦ if ↑l = ↑l₀ then 0 else -2 / (z - ↑l) ^ 3

case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[L - ↑l₀] z = ℘'[L - ↑l₀] z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ -(2 / (z - ↑l) ^ 3) = -(2 / (z - ↑l) ^ 3)

pp: case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ ¬↑l = L.ω₁ / 2

Tactic:
]

Goal state after:
case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ ¬↑l = L.ω₁ / 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_6
L : PeriodPair
⊢ ℘'[L] = ℘'[L]

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ DifferentiableOn ℂ ℘'[L - L.ω₁ / 2] (↑L.lattice)ᶜ

Tactic:
]

Goal state after:
L : PeriodPair
⊢ DifferentiableOn ℂ ℘'[L - L.ω₁ / 2] (↑L.lattice)ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ -∑' (c : ↥L.lattice), 2 / (-z - ↑((Equiv.neg ↥L.lattice) c)) ^ 3 = - -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

Tactic:
]

Goal state after:
L : PeriodPair
z : ℂ
⊢ -∑' (c : ↥L.lattice), 2 / (-z - ↑((Equiv.neg ↥L.lattice) c)) ^ 3 = - -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3