-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
lemma nonUnitalStarAlgHom_id {a : A} {φ : C(σₙ S a, S)₀ →⋆ₙₐ[S] A} {f : C(S, R)}
    (h : QuasispectrumRestricts a f) (h_id : φ (.id rfl) = a) :
    h.nonUnitalStarAlgHom φ (.id rfl) = a

Proof state:
case h.e'_2.h.e'_6.h
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id ⋯) = a
x : ↑(σₙ S a)
⊢ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
      x =
    (ContinuousMapZero.id ⋯) x

Tactic:
exact h.rightInvOn x.2

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id ⋯) = a
⊢ φ
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })) =
    a

Tactic:
convert h_id

Result:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id ⋯) = a
⊢ { toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
      ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }) =
    ContinuousMapZero.id ⋯

Proof state:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id ⋯) = a
⊢ { toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
      ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }) =
    ContinuousMapZero.id ⋯

Tactic:
ext x

Result:
case h.e'_2.h.e'_6.h
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id ⋯) = a
x : ↑(σₙ S a)
⊢ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
      x =
    (ContinuousMapZero.id ⋯) x

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id ⋯) = a
⊢ (nonUnitalStarAlgHom φ h) (ContinuousMapZero.id ⋯) = a

Tactic:
simp only [QuasispectrumRestricts.nonUnitalStarAlgHom_apply]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id ⋯) = a
⊢ φ
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })) =
    a