-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
lemma exp_eq_normedSpace_exp {a : A} (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
⊢ (cfcHom ha) { toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } =
    (cfcHom ⋯) (exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })

Tactic:
congr 1

Result:
case h.e_6.h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
⊢ { toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } =
    exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ }

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })

Tactic:
have h := (cfcHom_isClosedEmbedding (R := 𝕜) (show p a from ha)).continuous

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
⊢ cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
⊢ cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })

Tactic:
simp_rw [← map_exp 𝕜 _ h, cfc_apply (exp 𝕜) a ha]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
⊢ (cfcHom ha) { toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } =
    (cfcHom ⋯) (exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
⊢ cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })

Tactic:
have _ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a) := exp_continuous.continuousOn

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
⊢ cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })

Proof state:
case h.e_6.h.h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
a✝ : ↑(spectrum 𝕜 a)
⊢ { toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } a✝ =
    (exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ }) a✝

Tactic:
simp [exp_continuousMap_eq]

Result:
no goals

Proof state:
case h.e_6.h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
⊢ { toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } =
    exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ }

Tactic:
ext

Result:
case h.e_6.h.h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
h : Continuous ⇑(cfcHom ⋯)
x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)
a✝ : ↑(spectrum 𝕜 a)
⊢ { toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } a✝ =
    (exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ }) a✝

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (exp 𝕜) a = exp 𝕜 a

Tactic:
conv_rhs => rw [← cfc_id 𝕜 a ha, cfc_apply id a ha]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
p : A → Prop
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })