mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 0 < (↑π / a).re

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
⊢ 0 < (↑π / a).re
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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
⊢ HasFiniteIntegral (fun t ↦ f t maxr) (μ.restrict (Ioi 0))

Tactic:
]

Goal state after:
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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
⊢ HasFiniteIntegral (fun t ↦ f t maxr) (μ.restrict (Ioi 0))
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ -log ↑π / 2 / ↑√π = -log ↑π / 2 / ↑√π

Tactic:
]

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

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ 0 < a

Tactic:
]

Goal state after:
a : ℝ
ha : 0 < a
⊢ 0 < a
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_2
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
this : HasDerivAt (Gamma ∘ fun s ↦ s / 2) (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1

Tactic:
]

Goal state after:
case refine_2
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
this : HasDerivAt (Gamma ∘ fun s ↦ s / 2) (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ ↑(Nat.log b (n✝ + 1)) = ↑(Nat.log b (n✝ + 1))

pp: case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(n✝ + 1)

Tactic:
]

Goal state after:
case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(n✝ + 1)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ cfcₙ (fun x ↦ x.nnrpow p) a = cfcₙ (fun x ↦ x.nnrpow p) a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ ↑(Nat.log b ⌊r⌋₊) ≤ r

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ ↑(Nat.log b ⌊r⌋₊) ≤ r
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (↑b ^ ↑(Nat.clog b ⌈r⁻¹⌉₊))⁻¹ ≤ r

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (↑b ^ ↑(Nat.clog b ⌈r⁻¹⌉₊))⁻¹ ≤ r
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ ↑(Nat.log b ⌊r⌋₊).succ

Tactic:
]

Goal state after:
case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ ↑(Nat.log b ⌊r⌋₊).succ
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ ↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) < r⁻¹

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ ↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) < r⁻¹
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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ cfcₙ (fun x ↦ ↑(x.toNNReal.nnrpow p)) a = cfcₙ (fun r ↦ ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t r ∂μ) a

Tactic:
]

Goal state after:
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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ cfcₙ (fun x ↦ ↑(x.toNNReal.nnrpow p)) a = cfcₙ (fun r ↦ ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t r ∂μ) a
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ ↑n = ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ -↑n = -↑n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊

Tactic:
]

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ ↑(Nat.log b ⌊r₂⌋₊)

Tactic:
]

Goal state after:
case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ ↑(Nat.log b ⌊r₂⌋₊)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + log ↑(2 ^ 2 * π)) / 2 = -(↑γ + log (4 * ↑π)) / 2

Tactic:
]

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + log ↑(2 ^ 2 * π)) / 2 = -(↑γ + log (4 * ↑π)) / 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: x✝ : ℝ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ log x / log b = log x / log b

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb |b| x = logb |b| x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb b |x| = logb b |x|

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊
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 * b) c

Tactic:
]

Goal state after:
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 / b) c

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
⊢ cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
⊢ cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ log c / log a = log c / log a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hx : 0 < x
⊢ y * (log x / log b) = y * (log x / log b)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
k : ℕ
⊢ ↑k * (log x / log b) = ↑k * (log x / log b)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ x * log b = x * log b

pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Tactic:
]

Goal state after:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Tactic:
exact log_ne_zero_of_pos_of_ne_one b_pos b_ne_one

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ -↑(Nat.log b ⌊r⌋₊) = -↑(Nat.log b ⌊r⌋₊)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x

Tactic:
]

Goal state after:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ ↑(Nat.clog b ⌈r⁻¹⌉₊) = ↑(Nat.clog b ⌈r⁻¹⌉₊)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ |x| = x

Tactic:
]

Goal state after:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ |x| = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x

Tactic:
]

Goal state after:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ log b r⁻¹ = log b r⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ clog b r = clog b r

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ log b r = log b r

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(Nat.clog b n.succ) = ↑(Nat.clog b (n + 1))

pp: case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(n.succ - 1) < ↑(n + 1) ∧ ↑(n + 1) ≤ ↑n.succ

pp: case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ 1 ≤ ↑(n + 1)

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(n.succ - 1) < ↑(n + 1) ∧ ↑(n + 1) ≤ ↑n.succ

case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ 1 ≤ ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
hg : ContinuousOn (fun z ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (fun z ↦ 1 + z) (spectrum ℝ x)
hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
this : cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x = cfc (fun x ↦ t ^ (p - 1)) x - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x
⊢ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x) =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
⊢ x ≤ y ↔ x ≤ y

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ 1

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y

Tactic:
]

Goal state after:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Tactic:
]

Goal state after:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

Tactic:
]

Goal state after: