-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙHom_eq_cfcₙHom_of_cfcHom [ContinuousMapZero.UniqueHom R A] {a : A}
    (ha : p a) : cfcₙHom (R := R) ha = cfcₙHom_of_cfcHom R ha

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ cfcₙHom ha = cfcₙHom_of_cfcHom R ha

Tactic:
refine ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id
    (σₙ R a) ?_ _ _ ?_ ?_ ?_

Result:
case refine_1
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ ↑0 = 0

case refine_2
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ Continuous ⇑(cfcₙHom ha)

case refine_3
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ Continuous ⇑(cfcₙHom_of_cfcHom R ha)

case refine_4
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ (cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ?refine_1 } =
    (cfcₙHom_of_cfcHom R ha)
      { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ?refine_1 }

Proof state:
case refine_3
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ Continuous ⇑(cfcₙHom_of_cfcHom R ha)

Tactic:
exact (isClosedEmbedding_cfcₙHom_of_cfcHom ha).continuous

Result:
no goals

Proof state:
case refine_2
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ Continuous ⇑(cfcₙHom ha)

Tactic:
exact (cfcₙHom_isClosedEmbedding (R := R) ha).continuous

Result:
no goals

Proof state:
case refine_1
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ ↑0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_4
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ (cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    (cfcₙHom_of_cfcHom R ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ }

Tactic:
simpa only [cfcₙHom_id (R := R) ha] using (cfcHom_id ha).symm

Result:
no goals