mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
]

Goal state after:
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
]

Goal state after:
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -∑' (c : ↥L.lattice), 2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3 = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1

Tactic:
]

Goal state after:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ rexp 1 / √2 = rexp 1 / √2

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / √(1 - x ^ 2)

Tactic:
]

Goal state after:
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ ℘'[L] 0 = ℘'[L] 0

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.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ 0 = 0

pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬DifferentiableAt ℂ ℘[L] x

Tactic:
]

Goal state after:
case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬DifferentiableAt ℂ ℘[L] x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hderiv
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt f (deriv f x) x

Tactic:
apply DifferentiableAt.hasDerivAt

Goal state after:
case inr.hderiv
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f

Tactic:
]

Goal state after:
case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case succ
n✝ : ℕ
⊢ log ↑(n✝ + 1)! - (1 / 2 * log (2 * ↑(n✝ + 1)) + ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)) =
    log ↑(n✝ + 1)! - (1 / 2 * log (2 * ↑(n✝ + 1)) + ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1))

pp: case succ.hx
n✝ : ℕ
⊢ 0 < 2 * ↑(n✝ + 1)

pp: case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

pp: case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

Tactic:
]

Goal state after:
case succ.hx
n✝ : ℕ
⊢ 0 < 2 * ↑(n✝ + 1)

case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ ℘'[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = ∫ (x : ℝ) in a..b, deriv f x

Tactic:
]

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = ∫ (x : ℝ) in a..b, deriv f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioc a b, derivWithin f (Icc a b) x ∂volume = ∫ (x : ℝ) in Ioc a b, deriv f x ∂volume

Tactic:
]

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioc a b, derivWithin f (Icc a b) x ∂volume = ∫ (x : ℝ) in Ioc a b, deriv f x ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)

Tactic:
]

Goal state after:
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f

Tactic:
]

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))

Tactic:
]

Goal state after:
case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
⊢ ‖(↑l - x) ^ (-↑r)‖ ≤ ‖(↑l - x) ^ (-↑r)‖

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : b < a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ -(f a - f b) = f b - f a

Tactic:
]

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : b < a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ -(f a - f b) = f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
⊢ ‖f b - f a‖ₑ = ‖f b - f a‖ₑ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖∫ (x : ℝ) in Icc a b, deriv (⇑g ∘ f) x ∂volume‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ

Tactic:
]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖∫ (x : ℝ) in Icc a b, deriv (⇑g ∘ f) x ∂volume‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo a b), ‖deriv (⇑g ∘ f) a‖ₑ ≤ ‖deriv f a‖ₑ

Tactic:
]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo a b), ‖deriv (⇑g ∘ f) a‖ₑ ≤ ‖deriv f a‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x else (↑(i + 1) + 1) * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ (i + 3))⁻¹)

Tactic:
]

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x else (↑(i + 1) + 1) * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ (i + 3))⁻¹)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖(fderiv ℝ (⇑g) (f x)) (deriv f x)‖ₑ ≤ ‖deriv f x‖ₑ

pp: case hl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ (⇑g) (f x)

pp: case hf
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x

Tactic:
]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖(fderiv ℝ (⇑g) (f x)) (deriv f x)‖ₑ ≤ ‖deriv f x‖ₑ

case hl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ (⇑g) (f x)

case hf
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ ((2 * ↑(n + 1) + 1) ^ 2)⁻¹ < 1

Tactic:
]

Goal state after:
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ ((2 * ↑(n + 1) + 1) ^ 2)⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ (2 * ↑(k + 1) + 1)⁻¹ ≤ 1

Tactic:
]

Goal state after:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ (2 * ↑(k + 1) + 1)⁻¹ ≤ 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ (fun a ↦ ‖deriv f a‖ₑ) =ᵐ[volume.restrict (Ioo a b)] fun a_1 ↦ ‖derivWithin f (Icc a b) a_1‖ₑ

Tactic:
]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ (fun a ↦ ‖deriv f a‖ₑ) =ᵐ[volume.restrict (Ioo a b)] fun a_1 ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv f x‖ₑ = ‖deriv f x‖ₑ

Tactic:
]

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

Goal state before:
pp: case zero
⊢ 2 ≤ (1 + 1) ^ 2

Tactic:
]

Goal state after:
case zero
⊢ 2 ≤ (1 + 1) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ ∑' (x_1 : ↥L.lattice), (↑i + 2) * (((↑x_1 - x) ^ (i + 3))⁻¹ - if x_1 = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Summable fun l ↦ if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0

Tactic:
]

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ ∑' (x_1 : ↥L.lattice), (↑i + 2) * (((↑x_1 - x) ^ (i + 3))⁻¹ - if x_1 = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Summable fun l ↦ if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑0 + 1) + 1)) ^ 2 < 1

Tactic:
]

Goal state after:
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑0 + 1) + 1)) ^ 2 < 1
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ 1 / (12 * ↑n * (↑n + 1)) ≤ 1 / (4 * ↑n ^ 2)

Tactic:
]

Goal state after:
n : ℕ
⊢ 1 / (12 * ↑n * (↑n + 1)) ≤ 1 / (4 * ↑n ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
k : ℕ
hk : k ∈ range n
⊢ 1 / (12 * ↑(k + 1) * (↑(k + 1) + 1)) ≤ g k - g (k + 1)

Tactic:
]

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
k : ℕ
hk : k ∈ range n
⊢ 1 / (12 * ↑(k + 1) * (↑(k + 1) + 1)) ≤ g k - g (k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in Set.Ioc (-1) 1, NNReal.mk √(1 - x ^ 2)⁻¹ ⋯ • f x ∂volume =
    ∫ (x : ℝ) in Set.Ioc (-1) 1, f x * √(1 - x ^ 2)⁻¹ ∂volume

Tactic:
]

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in Set.Ioc (-1) 1, NNReal.mk √(1 - x ^ 2)⁻¹ ⋯ • f x ∂volume =
    ∫ (x : ℝ) in Set.Ioc (-1) 1, f x * √(1 - x ^ 2)⁻¹ ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : f 0 - f n ≤ g 0 - g n
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹

Tactic:
]

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : f 0 - f n ≤ g 0 - g n
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1)) ≤ 12⁻¹

Tactic:
]

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1)) ≤ 12⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: ⊢ IntegrableOn (fun x ↦ √(1 - x ^ 2)⁻¹) (Set.uIoc (-1) 1) volume

Tactic:
]

Goal state after:
⊢ IntegrableOn (fun x ↦ √(1 - x ^ 2)⁻¹) (Set.uIoc (-1) 1) volume
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ ContinuousOn f (Set.Icc (-1) 1)

Tactic:
]

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ ContinuousOn f (Set.Icc (-1) 1)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

pp: n : ℕ
this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 0 ≤ 2

pp: n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ √2 ≠ 0

Tactic:
]

Goal state after:
n : ℕ
this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

n : ℕ
this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 0 ≤ 2

n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ √2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f measureT

Tactic:
]

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f measureT
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: c : ℝ := 1 - 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ c ≤ log (stirlingSeq (n + 1))

Tactic:
]

Goal state after:
c : ℝ := 1 - 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ c ≤ log (stirlingSeq (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
]

Goal state after:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable (fun x ↦ f x * (↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)).toReal) (volume.restrict (Set.Ioc (-1) 1))

Tactic:
]

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable (fun x ↦ f x * (↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)).toReal) (volume.restrict (Set.Ioc (-1) 1))
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : 1 ≤ n
⊢ ↑n / (2 * ↑n + 1) = (fun n ↦ ↑n / (2 * ↑n + 1)) n

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2) ^ 2 /
        (↑(2 * n)! / (√(2 * ↑(2 * n)) * (↑(2 * n) / rexp 1) ^ (2 * n))) ^ 2 *
      (↑n / (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2) ^ 2 /
        (↑(2 * n)! / (√(2 * ↑(2 * n)) * (↑(2 * n) / rexp 1) ^ (2 * n))) ^ 2 *
      (↑n / (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, -(f x * √(1 - x ^ 2)⁻¹) = ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹

Tactic:
]

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, -(f x * √(1 - x ^ 2)⁻¹) = ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, ((fun θ ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - x ^ 2))

pp: case hf
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))

pp: case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

pp: case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0

Tactic:
]

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, ((fun θ ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - x ^ 2))

case hf
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))

case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: 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.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
⊢ Summable ((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm)

Tactic:
]

Goal state after:
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.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
⊢ Summable ((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm)