-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙHom_eq_cfcₙ_extend {a : A} (g : R → R) (ha : p a) (f : C(σₙ R a, R)₀) :
    cfcₙHom 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
x✝ : ↑(σₙ R a)
⊢ f x✝ = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g) x✝

Tactic:
simp [Subtype.val_injective.extend_apply]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
⊢ (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a

Tactic:
have hg : ContinuousOn (Function.extend Subtype.val f g) (σₙ 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
⊢ (cfcₙHom 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a

Tactic:
have h : f = (σₙ 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
⊢ (cfcₙHom 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
hg0 : Function.extend Subtype.val (⇑f) g 0 = 0
⊢ (cfcₙHom ha) f =
    (cfcₙHom ha)
      { toFun := (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g), continuous_toFun := ⋯, map_zero' := hg0 }

Tactic:
congr!

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
⊢ f 0 = ↑0

Tactic:
exact map_zero f

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
⊢ Function.extend Subtype.val (⇑f) g 0 = 0

Tactic:
rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_apply]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
⊢ f 0 = ↑0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
⊢ (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a

Tactic:
have hg0 : (Function.extend Subtype.val f g) 0 = 0 := by
  rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_apply]
  exact map_zero f

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
hg0 : Function.extend Subtype.val (⇑f) g 0 = 0
⊢ (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a