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

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

Tactic:
have ha₃ : ContinuousOn Real.log (spectrum ℝ a) := by
  have : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by peel ha₂ with x hx h; exact h.ne'
  fun_prop (disch := assumption)

Result:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
ha₃ : ContinuousOn Real.log (spectrum ℝ a)
⊢ exp ℝ (log a) = a

Proof state:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
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
inst✝ : CompleteSpace A
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
inst✝ : CompleteSpace A
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
inst✝ : CompleteSpace A
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
⊢ ContinuousOn Real.log (spectrum ℝ 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
inst✝ : CompleteSpace A
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn Real.log (spectrum ℝ a)

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

Tactic:
fun_prop

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
ha₃ : ContinuousOn Real.log (spectrum ℝ a)
⊢ cfc (fun x => Real.exp (Real.log x)) a = a

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

Result:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
ha₃ : ContinuousOn Real.log (spectrum ℝ a)
⊢ cfc (fun x => Real.exp (Real.log x)) a = cfc id a

Proof state:
case h.h
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
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

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

Tactic:
rw [← real_exp_eq_normedSpace_exp .log, log, ← cfc_comp' Real.exp Real.log a (by fun_prop) ha₃]

Result:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
ha₃ : ContinuousOn Real.log (spectrum ℝ a)
⊢ cfc (fun x => Real.exp (Real.log x)) a = a

Proof state:
case funProp.discharger
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
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