-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
case :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
    p ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g)
case₁ :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
    q ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g) ∧
      QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
        ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
        (⇑f : (a : S) → R)
case₂ :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
    QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) (⇑f : (a : S) → R)
case₃ :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀) (s : S)
    (hs :
      s ∈
        quasispectrum.{u_2, u_3} S (A := A)
          ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)),
    (algebraMap R S : (a : R) → S) ((f : (a : S) → R) s : R) = s
case₄ :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀) (s : S)
    (hs :
      Membership.mem (γ := Set S)
        (range (ι := (↑(σₙ S a) : Type u_2))
          (⇑(comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
                (g.comp
                  {
                    toFun :=
                      Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
                    continuous_toFun := ⋯, map_zero' := ⋯ :
                    ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) :
            (a : (↑(σₙ S a) : Type u_2)) → S))
        s),
    (algebraMap R S : (a : R) → S) ((f : (a : S) → R) s : R) = s
case₅ :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀) (r : (↑(σₙ S a) : Type u_2)),
    Eq.{u_2 + 1} (α := S)
      ((algebraMap R S : (a : R) → S)
          ((f : (a : S) → R)
              ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
                      (g.comp
                        {
                          toFun :=
                            Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a)
                              (⇑f : (a : S) → R) ⋯,
                          continuous_toFun := ⋯, map_zero' := ⋯ :
                          ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }) :
                    (a : (↑(σₙ S a) : Type u_2)) → S)
                  r :
                S) :
            R) :
        S)
      ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
              (g.comp
                {
                  toFun :=
                    Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
                  continuous_toFun := ⋯, map_zero' := ⋯ :
                  ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }) :
            (a : (↑(σₙ S a) : Type u_2)) → S)
          r :
        S)
⊢ ∀ (f_1 : C((↑(σₙ R a) : Type u_1), R)₀),
    p ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f_1)

Tactic:
case predicate_hom =>
      intro g
      rw [h]
      refine ⟨cfcₙHom_predicate _ _, ?_⟩
      refine { rightInvOn := fun s hs ↦ ?_, left_inv := ((h a).mp ha).2.left_inv }
      rw [nonUnitalStarAlgHom_apply,
        cfcₙHom_map_quasispectrum] at hs
      obtain ⟨r, rfl⟩ := hs
      simp [((h a).mp ha).2.left_inv _]

Premises used: cfcₙHom_map_quasispectrum, And.right, QuasispectrumRestricts.nonUnitalStarAlgHom_apply, Iff.mp, QuasispectrumRestricts.left_inv, rfl