awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id :
  (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A) (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
h₁ :
  Eq (α := C((↑(spectrum S a) : Type u_2), S))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
      (ContinuousMap.comp (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
        {
          toFun :=
            Subtype.map (p := fun (x : S) ↦ x ∈ spectrum S a) (q := fun (x : R) ↦ x ∈ spectrum R a) (⇑f : (a : S) → R)
              ⋯,
          continuous_toFun := ⋯ }))
    (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S))
⊢ (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A)
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
        (ContinuousMap.comp (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
          {
            toFun :=
              Subtype.map (p := fun (x : S) ↦ x ∈ spectrum S a) (q := fun (x : R) ↦ x ∈ spectrum R a) (⇑f : (a : S) → R)
                ⋯,
            continuous_toFun := ⋯ })) =
    a

Tactic:
convert! h_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id :
  (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A) (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
h₁ :
  ∀ (x : (↑(spectrum S a) : Type u_2)),
    Eq (α := S)
      ((ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
              (ContinuousMap.comp (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
                {
                  toFun :=
                    Subtype.map (p := fun (x : S) ↦ x ∈ spectrum S a) (q := fun (x : R) ↦ x ∈ spectrum R a)
                      (⇑f : (a : S) → R) ⋯,
                  continuous_toFun := ⋯ }) :
            (a : (↑(spectrum S a) : Type u_2)) → S)
          x :
        S)
      ((ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S) : (a : (↑(spectrum S a) : Type u_2)) → S) x : S)
⊢ Eq (α := C((↑(spectrum S a) : Type u_2), S))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
      (ContinuousMap.comp (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
        {
          toFun :=
            Subtype.map (p := fun (x : S) ↦ x ∈ spectrum S a) (q := fun (x : R) ↦ x ∈ spectrum R a) (⇑f : (a : S) → R)
              ⋯,
          continuous_toFun := ⋯ }))
    (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S))

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id :
  (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A) (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
x : (↑(spectrum S a) : Type u_2)
⊢ Eq (α := S)
    ((ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
            (ContinuousMap.comp (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
              {
                toFun :=
                  Subtype.map (p := fun (x : S) ↦ x ∈ spectrum S a) (q := fun (x : R) ↦ x ∈ spectrum R a)
                    (⇑f : (a : S) → R) ⋯,
                continuous_toFun := ⋯ }) :
          (a : (↑(spectrum S a) : Type u_2)) → S)
        x :
      S)
    ((ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S) : (a : (↑(spectrum S a) : Type u_2)) → S) x : S)

Tactic:
h.rightInvOn x.2

Premises used: SpectrumRestricts.rightInvOn, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id :
  (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A) (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
x : (↑(spectrum S a) : Type u_2)
⊢ Eq (α := S)
    ((ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
            (ContinuousMap.comp (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
              {
                toFun :=
                  Subtype.map (p := fun (x : S) ↦ x ∈ spectrum S a) (q := fun (x : R) ↦ x ∈ spectrum R a)
                    (⇑f : (a : S) → R) ⋯,
                continuous_toFun := ⋯ }) :
          (a : (↑(spectrum S a) : Type u_2)) → S)
        x :
      S)
    ((ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S) : (a : (↑(spectrum S a) : Type u_2)) → S) x : S)

Tactic:
exact h.rightInvOn x.2

Premises used: SpectrumRestricts.rightInvOn, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
hφ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := C((↑(spectrum S a) : Type u_2), S)) (β := A)
    (⇑φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A)
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
halg : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(spectrum R a) : Type u_1), R)) (β := A)
    (⇑(starAlgHom φ h) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
hφ.comp <| (postcomp_injective _ halg).comp <|
    h.homeomorph.symm.arrowCongr (.refl _) |>.injective

Premises used: SpectrumRestricts.homeomorph, Homeomorph.arrowCongr, Homeomorph.injective, Function.Injective.comp, Homeomorph.symm, Homeomorph.refl, ContinuousMap.postcomp_injective
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
hφ : Continuous[_, inst_18] (⇑φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A)
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ Continuous[_, inst_18] (⇑(starAlgHom φ h) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
hφ.comp <| (continuous_postcomp _).comp (continuous_precomp _)

Premises used: ContinuousMap.continuous_postcomp, Continuous.comp, ContinuousMap.continuous_precomp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : CompleteSpace R
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
hφ :
  IsClosedEmbedding.{u_2, u_3} (X := C((↑(spectrum S a) : Type u_2), S)) (Y := A)
    (⇑φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A)
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(spectrum R a) : Type u_1), R)) (Y := A)
    (⇑(starAlgHom φ h) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
hφ.comp <| IsUniformEmbedding.isClosedEmbedding <| .comp
    (ContinuousMap.isUniformEmbedding_comp _ halg)
    (UniformEquiv.arrowCongr h.homeomorph.symm (.refl _) |>.isUniformEmbedding)

Premises used: IsUniformEmbedding.comp, Topology.IsClosedEmbedding.comp, UniformEquiv.arrowCongr, SpectrumRestricts.homeomorph, ContinuousMap.isUniformEmbedding_comp, UniformEquiv.refl, Homeomorph.symm, IsUniformEmbedding.isClosedEmbedding, UniformEquiv.isUniformEmbedding
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
⊢ CompactSpace.{u_2} (↑(spectrum S a) : Type u_2)

Tactic:
have := ContinuousFunctionalCalculus.compactSpace_spectrum (R := S) a
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
this : CompactSpace.{u_2} (↑(spectrum S a) : Type u_2)
rw : ∀ (this : IsCompact (spectrum S a)), IsCompact (spectrum R a)
⊢ CompactSpace.{u_1} (↑(spectrum R a) : Type u_1)

Tactic:
rw [← isCompact_iff_compactSpace] at this ⊢

Premises used: isCompact_iff_compactSpace
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
this : IsCompact (spectrum S a)
⊢ IsCompact (spectrum R a)

Tactic:
simpa using halg.isCompact_preimage this

Premises used: Topology.IsClosedEmbedding.isCompact_preimage
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ ∃ (φ : C((↑(spectrum R a) : Type u_1), R) →⋆ₐ[R] A),
    Continuous[_, inst_18] (⇑φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) ∧
      Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(spectrum R a) : Type u_1), R)) (β := A)
          (⇑φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) ∧
        (φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
              (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
            a ∧
          (∀ (f : C((↑(spectrum R a) : Type u_1), R)),
              spectrum.{u_1, u_3} R (A := A) ((φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) =
                range (ι := (↑(spectrum R a) : Type u_1)) (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R)) ∧
            ∀ (f : C((↑(spectrum R a) : Type u_1), R)), p ((φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)

Tactic:
⟨((h a).mp ha).2.starAlgHom (cfcHom ((h a).mp ha).1 (R := S)),
      ?hom_continuous, ?hom_injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩

Premises used: cfcHom, And.right, And.left, And.intro, Exists.intro, Iff.mp, SpectrumRestricts.starAlgHom
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
refine : Continuous[_, inst_18] (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
refine₁ :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(spectrum R a) : Type u_1), R)) (β := A)
    (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
refine₂ :
  (starAlgHom (cfcHom (p := q) ⋯) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    a
refine₃ :
  ∀ (f_1 : C((↑(spectrum R a) : Type u_1), R)),
    spectrum.{u_1, u_3} R (A := A)
        ((starAlgHom (cfcHom (p := q) ⋯) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f_1 : A) =
      range (ι := (↑(spectrum R a) : Type u_1)) (⇑f_1 : (a : (↑(spectrum R a) : Type u_1)) → R)
refine₄ :
  ∀ (f_1 : C((↑(spectrum R a) : Type u_1), R)),
    p ((starAlgHom (cfcHom (p := q) ⋯) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f_1)
⊢ ∃ (φ : C((↑(spectrum R a) : Type u_1), R) →⋆ₐ[R] A),
    Continuous[_, inst_18] (⇑φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) ∧
      Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(spectrum R a) : Type u_1), R)) (β := A)
          (⇑φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) ∧
        (φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
              (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
            a ∧
          (∀ (f : C((↑(spectrum R a) : Type u_1), R)),
              spectrum.{u_1, u_3} R (A := A) ((φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) =
                range (ι := (↑(spectrum R a) : Type u_1)) (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R)) ∧
            ∀ (f : C((↑(spectrum R a) : Type u_1), R)), p ((φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)

Tactic:
refine ⟨((h a).mp ha).2.starAlgHom (cfcHom ((h a).mp ha).1 (R := S)),
      ?hom_continuous, ?hom_injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ Continuous[_, inst_18] (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
((h a).mp ha).2.continuous_starAlgHom (cfcHom_continuous ((h a).mp ha).1)

Premises used: cfcHom_continuous, SpectrumRestricts.continuous_starAlgHom, And.right, And.left, Iff.mp
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ Continuous[_, inst_18] (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
exact ((h a).mp ha).2.continuous_starAlgHom (cfcHom_continuous ((h a).mp ha).1)

Premises used: cfcHom_continuous, SpectrumRestricts.continuous_starAlgHom, And.right, And.left, Iff.mp
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ Continuous[_, inst_18] (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
case hom_continuous =>
      exact ((h a).mp ha).2.continuous_starAlgHom (cfcHom_continuous ((h a).mp ha).1)

Premises used: cfcHom_continuous, SpectrumRestricts.continuous_starAlgHom, And.right, And.left, Iff.mp
-- 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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : TopologicalSpace A
inst_19 : ContinuousFunctionalCalculus S A q
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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(spectrum R a) : Type u_1), R)) (β := A)
    (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
((h a).mp ha).2.starAlgHom_injective (cfcHom_injective ((h a).mp ha).1) halg.injective

Premises used: cfcHom_injective, Topology.IsClosedEmbedding.toIsEmbedding, And.right, And.left, Topology.IsEmbedding.injective, Iff.mp, SpectrumRestricts.starAlgHom_injective