-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
lemma log_pow (n : ℕ) (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x)
    (ha₁ : IsSelfAdjoint a

Proof state:
case funProp.discharger
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn Real.log (spectrum ℝ a)

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
peel ha₂ with x hx h

Result:
case h.h
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
x : ℝ
hx : x ∈ spectrum ℝ a
h : 0 < x
⊢ x ≠ 0

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
⊢ ContinuousOn Real.log ((fun x => x ^ n) '' spectrum ℝ a)

Tactic:
fun_prop (disch := aesop)

Result:
no goals

Proof state:
case funProp.discharger
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
⊢ ∀ x ∈ (fun x => x ^ n) '' spectrum ℝ a, x ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x => x ^ n) '' spectrum ℝ a)
⊢ cfc (fun x => Real.log (x ^ n)) a = n • cfc Real.log a

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

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
⊢ log (a ^ n) = n • log a

Tactic:
have : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by peel ha₂ with x hx h; exact h.ne'

Result:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ log (a ^ n) = n • log a

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ log (a ^ n) = n • log a

Tactic:
have ha₂' : ContinuousOn Real.log (spectrum ℝ a) := by fun_prop (disch := assumption)

Result:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
⊢ log (a ^ n) = n • log a

Proof state:
case h.h
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
x : ℝ
hx : x ∈ spectrum ℝ a
h : 0 < x
⊢ x ≠ 0

Tactic:
exact h.ne'

Result:
no goals