-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp (g f : R → R) (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict (g ∘ f), continuous_toFun := ⋯ } =
    (cfcHom ⋯)
      ({ toFun := (spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })).restrict g,
            continuous_toFun := ⋯ }.comp
        ?f')

case f'
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ C(↑(spectrum R a), ↑(spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })))

case hff'
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ ∀ (x : ↑(spectrum R a)), { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } x = ↑(?f' x)

Tactic:
swap

Result:
case f'
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ C(↑(spectrum R a), ↑(spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })))

R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict (g ∘ f), continuous_toFun := ⋯ } =
    (cfcHom ⋯)
      ({ toFun := (spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })).restrict g,
            continuous_toFun := ⋯ }.comp
        ?f')

case hff'
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ ∀ (x : ↑(spectrum R a)), { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } x = ↑(?f' x)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ ContinuousOn g (spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }))

Tactic:
convert hg

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ (spectrum R a).restrict f x ∈ f '' spectrum R a

Tactic:
use x.1

Result:
case h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ ↑x ∈ spectrum R a ∧ f ↑x = (spectrum R a).restrict f x