mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right✝ : y < r
⊢ y ^ (↑(Module.finrank ℝ E) - 1 - α) * C = y ^ (↑(Module.finrank ℝ E - 1) + -α) * C

Tactic:
]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right✝ : y < r
⊢ y ^ (↑(Module.finrank ℝ E) - 1 - α) * C = y ^ (↑(Module.finrank ℝ E - 1) + -α) * C
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint : IntegrableOn (fun x ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ
⊢ IntegrableOn f (ball 0 r) μ

Tactic:
]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint : IntegrableOn (fun x ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ
⊢ IntegrableOn f (ball 0 r) μ
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
⊢ y ∈ Ioo 0 1 • (ball x ε ∩ sphere 0 1)

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
⊢ y ∈ Ioo 0 1 • (ball x ε ∩ sphere 0 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ ∀ (k : Set E), IsCompact k → IntegrableOn f k μ

Tactic:
]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ ∀ (k : Set E), IsCompact k → IntegrableOn f k μ
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ dist u x < ε

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ dist u x < ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.nthRoot 0 = 0

Tactic:
rcases n with _ | _ | _

Goal state after:
case zero
h : 0 ≠ 0
⊢ nthRoot 0 0 = 0

case succ.zero
h : 0 + 1 ≠ 0
⊢ (0 + 1).nthRoot 0 = 0

case succ.succ
n✝ : ℕ
h : n✝ + 1 + 1 ≠ 0
⊢ (n✝ + 1 + 1).nthRoot 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n : ℕ
⊢ n.nthRoot 1 = 1

Tactic:
rcases n with _ | _ | _

Goal state after:
case zero
⊢ nthRoot 0 1 = 1

case succ.zero
⊢ (0 + 1).nthRoot 1 = 1

case succ.succ
n✝ : ℕ
⊢ (n✝ + 1 + 1).nthRoot 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
⊢ (if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
        go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
      else guess) ^
      (n + 2) ≤
    a

Tactic:
]

Goal state after:
case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
⊢ (if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
        go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
      else guess) ^
      (n + 2) ≤
    a
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a : ℕ
⊢ n.nthRoot a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0

Tactic:
rcases n with _ | _ | _

Goal state after:
case zero
a : ℕ
⊢ nthRoot 0 a ^ 0 ≤ a ↔ 0 ≠ 0 ∨ a ≠ 0

case succ.zero
a : ℕ
⊢ (0 + 1).nthRoot a ^ (0 + 1) ≤ a ↔ 0 + 1 ≠ 0 ∨ a ≠ 0

case succ.succ
a n✝ : ℕ
⊢ (n✝ + 1 + 1).nthRoot a ^ (n✝ + 1 + 1) ≤ a ↔ n✝ + 1 + 1 ≠ 0 ∨ a ≠ 0
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ ε / 4 + ε / 4 = ε / 2

Tactic:
by ring

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l ^ 2 - (s - l) ^ 2) / ((s - l) ^ 2 * l ^ 2)‖ = ‖(l ^ 2 - (s - l) ^ 2) / ((s - l) ^ 2 * l ^ 2)‖

pp: case hb
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ (s - l) ^ 2 ≠ 0

pp: case hd
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ l ^ 2 ≠ 0

Tactic:
]

Goal state after:
case hb
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ (s - l) ^ 2 ≠ 0

case hd
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ l ^ 2 ≠ 0
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
hyx : dist y x < ε / 2
H : u - y = (1 - ‖y‖) • u
⊢ dist u y ≤ dist x y

Tactic:
simpa [dist_eq_norm_sub, H, norm_smul, abs_of_nonneg, hy₁.le, hu₁, hx]
      using dist_triangle x y 0

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
⊢ (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n

Tactic:
]

Goal state after:
n a b : ℕ
hb : b ≠ 0
⊢ (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ 0 ≤ ↑a ^ (n + 1) + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n

Tactic:
]

Goal state after:
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ 0 ≤ ↑a ^ (n + 1) + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hab
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖l - s‖

Tactic:
]

Goal state after:
case hab
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖l - s‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))

Tactic:
]

Goal state after:
case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖

Tactic:
]

Goal state after:
case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a <
    ((if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
          go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
        else guess) +
        1) ^
      (n + 2)

Tactic:
]

Goal state after:
case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a <
    ((if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
          go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
        else guess) +
        1) ^
      (n + 2)
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 1 / (-z - ↑((Equiv.neg ↥L.lattice) c)) ^ 2 - 1 / ↑((Equiv.neg ↥L.lattice) c) ^ 2) =
    ∑' (l : ↥L.lattice), if ↑l = -l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ^ n ≤ a ^ n ↔ b ≤ a

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ^ n ≤ a ^ n ↔ b ≤ a
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (Ioo 0 1 • (ball (↑x) ε ∩ sphere 0 1))

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (Ioo 0 1 • (ball (↑x) ε ∩ sphere 0 1))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℕ
⊢ x ^ n = x ^ n

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (ball ((1 - ε / 4) • ↑x) (ε / 4))

pp: case hx
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ‖↑x‖ = 1

pp: case hε
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ 0 < ε

pp: case hε2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ε ≤ 2

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (ball ((1 - ε / 4) • ↑x) (ε / 4))

case hx
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ‖↑x‖ = 1

case hε
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ 0 < ε

case hε2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ε ≤ 2
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 1 / (z - ↑b) ^ 2 - 1 / ↑b ^ 2) +
        if ↑b = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0) =
    ℘[L] z

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

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

Tactic:
]

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

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

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

Goal state before:
pp: case refine_2
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ ↑((n + 1) * n !) = ↑n ! * (↑n + 1)

Tactic:
]

Goal state after:
case refine_2
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ ↑((n + 1) * n !) = ↑n ! * (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - ↑l₀] z = ℘[L - ↑l₀] z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) + (1 / ↑l₀ ^ 2 - 1 / (z - ↑l₀) ^ 2)

Tactic:
]

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - ↑l₀] z = ℘[L - ↑l₀] z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) + (1 / ↑l₀ ^ 2 - 1 / (z - ↑l₀) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

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

Tactic:
]

Goal state after:
case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
x✝ : ℂ
⊢ ¬↑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), (1 / (-z - ↑((Equiv.neg ↥L.lattice) c)) ^ 2 - 1 / ↑((Equiv.neg ↥L.lattice) c) ^ 2) =
    ∑' (l : ↥L.lattice), (1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2)

Tactic:
]

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

Goal state before:
pp: case pos
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b n *
        ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))) /
      regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))

Tactic:
]

Goal state after:
case pos
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b n *
        ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))) /
      regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 16 * ‖↑l - s‖ ^ 3

pp: case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

pp: case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3

Tactic:
]

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 16 * ‖↑l - s‖ ^ 3

case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ a.card * (Multiset.map (fun x ↦ x / ↑n + 1) a).prod /
      (↑n ^ b.card * (Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (↑n + 1)) =
    ↑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:
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ a.card * (Multiset.map (fun x ↦ x / ↑n + 1) a).prod /
      (↑n ^ b.card * (Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (↑n + 1)) =
    ↑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)⁻¹))
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ ↑(toSphereBallBound (dim E) ε) * (μ (ball 0 1)).toReal ≤ ↑(toSphereBallBound (dim E) ε) * (μ (ball 0 1)).toReal

pp: case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ μ.toSphere (ball x ε) ≠ ∞

Tactic:
]

Goal state after:
case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ μ.toSphere (ball x ε) ≠ ∞
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * (2 * ‖↑l - s‖) ^ 3 = 16 * ‖↑l - s‖ ^ 3

Tactic:
by ring

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

Goal state before:
pp: case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ ↑a.card = ↑n ^ (↑(b.card + 1) + (↑a.card - ↑b.card - 1))

Tactic:
]

Goal state after:
case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ ↑a.card = ↑n ^ (↑(b.card + 1) + (↑a.card - ↑b.card - 1))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n * ↑n ^ b.card * ↑n ^ (↑a.card - ↑b.card - 1) * (Multiset.map (fun x ↦ (x + ↑n) / ↑n) a).prod =
    ↑n * (Multiset.map (fun x ↦ (x + ↑n) / ↑n) a).prod * ↑n ^ b.card * ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
by ring

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

Goal state before:
pp: a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → regularizedHGFunCoeff a b b_1 ≠ 0

Tactic:
]

Goal state after:
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → regularizedHGFunCoeff a b b_1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case h
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
h' : (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m
⊢ False

Tactic:
]

Goal state after:
case h
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
h' : (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m
⊢ False