-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfcHom_eq_cfc_extend {a : A} (g : R → R) (ha : p a) (f : C(spectrum R a, R)) :
    cfcHom ha f = cfc (Function.extend Subtype.val f g) 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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
⊢ ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)

Tactic:
ext

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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
x✝ : ↑(spectrum R a)
⊢ f x✝ = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g) 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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (spectrum R a)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a

Tactic:
rw [cfc_apply ..]

Result:
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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (spectrum R a)
⊢ (cfcHom ha) f =
    (cfcHom ha) { toFun := (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g), continuous_toFun := ⋯ }

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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a

Tactic:
have hg : ContinuousOn (Function.extend Subtype.val f g) (spectrum R a) :=
  continuousOn_iff_continuous_restrict.mpr <| h ▸ map_continuous f

Result:
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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (spectrum R a)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) 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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (spectrum R a)
⊢ (cfcHom ha) f =
    (cfcHom ha) { toFun := (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g), continuous_toFun := ⋯ }

Tactic:
congr!

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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a

Tactic:
have h : f = (spectrum R a).restrict (Function.extend Subtype.val f g) := by
  ext; simp [Subtype.val_injective.extend_apply]

Result:
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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a

Proof state:
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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
x✝ : ↑(spectrum R a)
⊢ f x✝ = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g) x✝

Tactic:
simp [Subtype.val_injective.extend_apply]

Result:
no goals