awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)
rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (x ^ n)) a = n • cfc (p := IsSelfAdjoint) Real.log a
⊢ log (a ^ n) = n • log a

Tactic:
rw [log, ← cfc_pow_id (R := ℝ) a n ha₁, ← cfc_comp' Real.log (· ^ n) a ha₂'', log]

Premises used: cfc_comp', Real.log, HPow.hPow, CFC.log, cfc_pow_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)
simp_rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑n : ℝ) * Real.log x) a = n • cfc (p := IsSelfAdjoint) Real.log a
simp_rw₁ :
  cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑n : ℝ) * Real.log x) a =
    HSMul.hSMul (α := ℝ) (↑n : ℝ) (cfc (p := IsSelfAdjoint) Real.log a)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (x ^ n)) a = n • cfc (p := IsSelfAdjoint) Real.log a

Tactic:
simp_rw [Real.log_pow, ← Nat.cast_smul_eq_nsmul ℝ n, cfc_const_mul (n : ℝ) Real.log a ha₂']

Premises used: Real, Nat.cast, Real.log, Nat.cast_smul_eq_nsmul, Real.log_pow, cfc_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
n : ℕ
a : A
ha : IsStrictlyPositive a
⊢ log (a ^ n) = n • log a

Tactic:
grind [log_pow]

Premises used: CFC.log_pow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ Real.exp '' spectrum ℝ a, x ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
funProp : ∀ x ∈ Real.exp '' spectrum ℝ a, x ≠ 0
⊢ ContinuousOn Real.log (Real.exp '' spectrum ℝ a)

Tactic:
fun_prop (disch := simp)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ContinuousOn Real.log (Real.exp '' spectrum ℝ a)

Tactic:
have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := simp)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (Real.exp x)) a = a
⊢ log (exp a) = a

Tactic:
rw [log, ← real_exp_eq_normedSpace_exp, ← cfc_comp' Real.log Real.exp a hcont]

Premises used: cfc_comp', Real.exp, Real.log, CFC.log, CFC.real_exp_eq_normedSpace_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (Real.exp x)) a = a

Tactic:
simp [cfc_id' (R := ℝ) a]

Premises used: Real, cfc_id'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
have ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn Real.exp (Real.log '' spectrum ℝ a)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
rw : cfc (R := ℝ) (p := IsSelfAdjoint) id a
| a

Tactic:
rw [← cfc_id (R := ℝ) a]

Premises used: Real, cfc_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
conv_rhs : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.exp (Real.log x)) a = cfc (R := ℝ) (p := IsSelfAdjoint) id a
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.exp (Real.log x)) a = a

Tactic:
conv_rhs => rw [← cfc_id (R := ℝ) a]

Premises used: Real, cfc_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.exp (Real.log x)) a = cfc (R := ℝ) (p := IsSelfAdjoint) id a

Tactic:
cfc_congr fun x hx => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
refine : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a), Real.exp (Real.log x) = id x
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.exp (Real.log x)) a = cfc (R := ℝ) (p := IsSelfAdjoint) id a

Tactic:
refine cfc_congr fun x hx => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ Real.exp (Real.log x) = id x

Tactic:
grind [Real.exp_log]

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : CompleteSpace A
⊢ Membership.mem (γ := Filter ℝ)
    (nhdsSet (⋃ (x : A), ⋃ (_ : Membership.mem (γ := Set A) {a : A | IsSelfAdjoint a ∧ IsUnit a} x), spectrum ℝ (id x)))
    {0}ᶜ

Tactic:
simpa using fun _ _ ↦ spectrum.zero_notMem ℝ

Premises used: Real, spectrum.zero_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ Tendsto (fun (p : ℝ) ↦ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a) (𝓝[>] 0) (𝓝 (log a))

Tactic:
tendsto_cfc_fun ?tendsto ?cont

Premises used: tendsto_cfc_fun, CFC.log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
refine : TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
refine₁ : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ x⁻¹ * (x_1 ^ x - 1)) (spectrum ℝ a)
⊢ Tendsto (fun (p : ℝ) ↦ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a) (𝓝[>] 0) (𝓝 (log a))

Tactic:
refine tendsto_cfc_fun ?tendsto ?cont

Premises used: tendsto_cfc_fun
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
p : ℝ
⊢ 0 ≤ p

Tactic:
grind -abstractProof
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
p : ℝ
⊢ (↑0 : ℝ) ≤ p

Tactic:
grind -abstractProof
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
p : ℝ
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
grind -abstractProof
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
p : ℝ
funProp : 0 ≤ p
funProp₁ : (↑0 : ℝ) ≤ p
funProp₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) (spectrum ℝ a)

Tactic:
fun_prop (disch := grind -abstractProof)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ x⁻¹ * (x_1 ^ x - 1)) (spectrum ℝ a)

Tactic:
exact .of_forall fun p ↦ by fun_prop (disch := grind -abstractProof)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ x⁻¹ * (x_1 ^ x - 1)) (spectrum ℝ a)

Tactic:
case cont =>
    exact .of_forall fun p ↦ by fun_prop (disch := grind -abstractProof)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a : A | IsStrictlyPositive a}
f : (p x : ℝ) → ℝ := fun (p x : ℝ) ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
⊢ TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)

Tactic:
have hmain := Real.tendstoLocallyUniformlyOn_rpow_sub_one_log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a : A | IsStrictlyPositive a}
f : (p x : ℝ) → ℝ := fun (p x : ℝ) ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)
⊢ ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain

Premises used: isOpen_Ioi, tendstoLocallyUniformlyOn_iff_forall_isCompact
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a : A | IsStrictlyPositive a}
f : (p x : ℝ) → ℝ := fun (p x : ℝ) ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K
⊢ spectrum ℝ a ⊆ Set.Ioi 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a : A | IsStrictlyPositive a}
f : (p x : ℝ) → ℝ := fun (p x : ℝ) ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K
⊢ IsCompact (spectrum ℝ a)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a : A | IsStrictlyPositive a}
f : (p x : ℝ) → ℝ := fun (p x : ℝ) ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

Tactic:
exact hmain (spectrum ℝ a) (by grind) (by grind)

Premises used: Real, spectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
case case₁ case₂ case₃ : TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
case₄ :
  ∀ (hmain : TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)),
    TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
case₅ :
  ∀ (hmain : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K),
    TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

Tactic:
case tendsto =>
    let s := {a : A | IsStrictlyPositive a}
    let f (p : ℝ) (x : ℝ) := if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
    have hmain := Real.tendstoLocallyUniformlyOn_rpow_sub_one_log
    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain
    exact hmain (spectrum ℝ a) (by grind) (by grind)

Premises used: isOpen_Ioi, tendstoLocallyUniformlyOn_iff_forall_isCompact
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
rw :
  ∀ (x : A),
    Tendsto
      (fun (i : ℝ) ↦
        if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} x then
          cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) x
        else 0)
      (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} x then log x else 0))
⊢ Tendsto.{0, u_1} (β := (a : A) → A)
    (fun (p : ℝ) (a : A) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 fun (a : A) ↦ if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0)

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
pos :
  ∀ (ha : IsStrictlyPositive a),
    Tendsto
      (fun (i : ℝ) ↦
        if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
          cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
        else 0)
      (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))
neg :
  ∀ (ha : ¬IsStrictlyPositive a),
    Tendsto
      (fun (i : ℝ) ↦
        if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
          cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
        else 0)
      (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))
⊢ Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))

Tactic:
by_cases ha : IsStrictlyPositive a

Premises used: IsStrictlyPositive
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))

Tactic:
simpa [ha] using CFC.tendsto_cfc_rpow_sub_one_log ha

Premises used: CFC.tendsto_cfc_rpow_sub_one_log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : ¬IsStrictlyPositive a
⊢ Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
simp : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)
⊢ Eq.{u_1 + 1} (α := A)
    ((fun (a : A) ↦
        if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
          cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a
        else 0)
      a)
    ((fun (a : A) ↦ p⁻¹ • (a ^ p - 1)) a)

Tactic:
simp only [ha, ↓reduceIte, ← smul_eq_mul]

Premises used: reduceIte, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ 0 ≤ p

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ (↑0 : ℝ) ≤ p

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
funProp : 0 ≤ p
funProp₁ : (↑0 : ℝ) ≤ p
funProp₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p - 1) (spectrum ℝ a)

Tactic:
fun_prop (disch := grind)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
funProp : 0 ≤ p
funProp₁ : (↑0 : ℝ) ≤ p
funProp₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) (spectrum ℝ a)

Tactic:
fun_prop (disch := grind)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
rw : p⁻¹ • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p - 1) a = p⁻¹ • (a ^ p - 1)
rw₁ :
  p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a) =
    p⁻¹ • (a ^ p - 1)
rw₂ : p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - 1) = p⁻¹ • (a ^ p - 1)
rw₃ rw₄ :
  p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - 1) =
    p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - 1)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)

Tactic:
rw [cfc_smul _ (hf := by fun_prop (disch := grind)),
    cfc_sub _ _ (hf := by fun_prop (disch := grind)),
    cfc_const_one .., rpow_eq_cfc_real ..]

Premises used: cfc_const_one, cfc_sub, cfc_smul, CFC.rpow_eq_cfc_real
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
⊢ Set.EqOn g log s

Tactic:
simp +contextual [g, Set.EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
⊢ Set.EqOn g log s

Tactic:
have hg : s.EqOn g (log (A := A)) := by simp +contextual [g, Set.EqOn]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ MonotoneOn log {a : A | IsStrictlyPositive a}

Tactic:
MonotoneOn.congr ?_ hg

Premises used: MonotoneOn.congr