mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case convert_2.convert_2.e_a
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this✝ : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
this : Continuous v₂
⊢ (2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, (2 * ↑n + 1) * (f x ^ n * v₂ x)) -
      2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, 2 * ↑n * (f x ^ (n - 1) * v₂ x) =
    2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
[

Goal state after:
case convert_2.convert_2.e_a
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this✝ : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
this : Continuous v₂
⊢ (2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, (2 * ↑n + 1) * (f x ^ n * v₂ x)) -
      2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, 2 * ↑n * (f x ^ (n - 1) * v₂ x) =
    2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ConcaveOn ℝ (fun a ↦ Ici 0 a) fun a ↦ sqrt a

Tactic:
[

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ConcaveOn ℝ (fun a ↦ Ici 0 a) fun a ↦ sqrt a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ConcaveOn ℝ (fun a ↦ Ici 0 a) fun a ↦ sqrt a

Tactic:
simp_rw [sqrt_eq_nnrpow]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ConcaveOn ℝ (fun a ↦ Ici 0 a) fun a ↦ a ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ Monotone fun a ↦ a ^ ↑q

Tactic:
[

Goal state after:
case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ Monotone fun a ↦ a ^ ↑q
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ ↑q

Tactic:
[

Goal state after:
case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ ↑q
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a | IsStrictlyPositive a}
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

Tactic:
let f (p : ℝ) (x : ℝ) := if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → ℝ → ℝ := fun p x ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
⊢ |∫ (x : ℝ) in a..b, x⁻¹ * δ| = δ * |log (b / a)|

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
⊢ |∫ (x : ℝ) in a..b, x⁻¹ * δ| = δ * |log (b / a)|
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
    (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x)

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
    (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this : (a • 1 + b • r) ^ (-1) ≤ a • 1 ^ (-1) + b • r ^ (-1)
⊢ (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)

Tactic:
[

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this : (a • 1 + b • r) ^ (-1) ≤ a • 1 ^ (-1) + b • r ^ (-1)
⊢ (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)

Tactic:
[

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
hδ : ball 0 δ ∩ Ioi 0 ⊆ {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2}
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
hδ : ball 0 δ ∩ Ioi 0 ⊆ {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2}
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < ∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / ↑i.factorial

Tactic:
[

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < ∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / ↑i.factorial
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
[

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Tactic:
[

Goal state after:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ eulerMascheroniSeq' n = ↑(harmonic n) - log ↑n

Tactic:
[

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ eulerMascheroniSeq' n = ↑(harmonic n) - log ↑n
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniConstant

Tactic:
by
  refine (strictMono_eulerMascheroniSeq (Nat.lt_succ_self n)).trans_le ?_
  apply strictMono_eulerMascheroniSeq.monotone.ge_of_tendsto tendsto_eulerMascheroniSeq

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂C • volume

Tactic:
[

Goal state after:
case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂C • volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹

Tactic:
[

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (p.rpowIntegrand₀₁ t) a = cfcₙ (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a

Tactic:
by
          refine cfcₙ_congr ?_
          refine Set.EqOn.mono hspec (rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one ht)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1))
⊢ Tendsto (fun x ↦ -x - (a * x ^ 2 + b * x)) atTop atTop

Tactic:
this

Goal state after:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1))
⊢ Tendsto (fun x ↦ x * (-a * x - (b + 1))) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ‖cexp (a * ↑x ^ 2 + b * ↑x)‖ = rexp (a.re * x ^ 2 + b.re * x)

Tactic:
[

Goal state after:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ‖cexp (a * ↑x ^ 2 + b * ↑x)‖ = rexp (a.re * x ^ 2 + b.re * x)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: case right
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : 0 < x
⊢ x ^ s = |x| ^ s

Tactic:
[

Goal state after:
case right
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : 0 < x
⊢ x ^ s = |x| ^ s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (fun x ↦ cexp (-a * ↑x ^ 2)) = fun x ↦ cexp (-a * ↑x ^ 2 + 0 * ↑x)

Tactic:
[

Goal state after:
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (fun x ↦ cexp (-a * ↑x ^ 2)) = fun x ↦ cexp (-a * ↑x ^ 2 + 0 * ↑x)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)

Tactic:
have h1 : 0 < (π * a).re := by
    rw [re_ofReal_mul]
    exact mul_pos pi_pos ha

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)) =O[cocompact ℝ] fun x ↦ |x| ^ (-2)

Tactic:
[

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)) =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)) =O[cocompact ℝ] fun x ↦ |x| ^ (-2)

Tactic:
this

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a)) =O[cocompact ℝ]
    fun x ↦ |x| ^ (-2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case e_a.e_a.e_a.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt (fun s ↦ 1 - 2 * s) (-2) (1 / 2)

Tactic:
[

Goal state after:
case e_a.e_a.e_a.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt (fun s ↦ 1 - 2 * s) (-2) (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x * y) = logb b x + logb b y

Tactic:
[

Goal state after:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x * y) = logb b x + logb b y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x / y) = logb b x - logb b y

Tactic:
[

Goal state after:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x / y) = logb b x - logb b y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
⊢ (logb a b)⁻¹ = logb b a

Tactic:
[

Goal state after:
a b : ℝ
⊢ (logb a b)⁻¹ = logb b a
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹

Tactic:
[

Goal state after:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

Tactic:
[

Goal state after:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ y ↔ b ^ y ≤ x

Tactic:
← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one,

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ b ^ y ≤ b ^ logb b x ↔ b ^ y ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x ≤ logb b y ↔ y ≤ b ^ x

Tactic:
← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one,

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ b ^ logb b y ≤ b ^ x ↔ y ≤ b ^ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: ⊢ AntitoneOn (fun x ↦ log x / √x) (Ici (rexp 2))

Tactic:
[

Goal state after:
⊢ AntitoneOn (fun x ↦ log x / √x) (Ici (rexp 2))
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
this : x = (fun ε ↦ ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Tactic:
this

Goal state after:
x : ℝ
this : x = (fun ε ↦ ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 ((fun ε ↦ ε.mulExpNegMulSq x) 0))
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
[

Goal state after:
b x : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : limsup (fun i ↦ ∫ (x : X), (const X ‖f‖ - f) x ∂μs i) L ≤ ∫ (x : X), (const X ‖f‖ - f) x ∂μ
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

Tactic:
[

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : limsup (fun i ↦ ∫ (x : X), (const X ‖f‖ - f) x ∂μs i) L ≤ ∫ (x : X), (const X ‖f‖ - f) x ∂μ
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L