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
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
g : C((↑(spectrum R a) : Type u_1), R)
s : S
hs :
  Membership.mem (γ := Set S)
    (range (ι := (↑(spectrum S a) : Type u_2))
      (⇑(ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
            (g.comp
              {
                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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) })) :
        (a : (↑(spectrum S a) : Type u_2)) → S))
    s
obtain :
  ∀ (r : (↑(spectrum S a) : Type u_2)),
    Eq.{u_2 + 1} (α := S)
      ((algebraMap R S : (a : R) → S)
          ((f : (a : S) → R)
              ((ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
                      (g.comp
                        {
                          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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) }) :
                    (a : (↑(spectrum S a) : Type u_2)) → S)
                  r :
                S) :
            R) :
        S)
      ((ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
              (g.comp
                {
                  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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) }) :
            (a : (↑(spectrum S a) : Type u_2)) → S)
          r :
        S)
⊢ (algebraMap R S : (a : R) → S) ((f : (a : S) → R) s : R) = s

Tactic:
obtain ⟨r, rfl⟩ := hs

Premises used: rfl
-- 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
g : C((↑(spectrum R a) : Type u_1), R)
r : (↑(spectrum S a) : Type u_2)
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((f : (a : S) → R)
            ((ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
                    (g.comp
                      {
                        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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) }) :
                  (a : (↑(spectrum S a) : Type u_2)) → S)
                r :
              S) :
          R) :
      S)
    ((ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
            (g.comp
              {
                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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) }) :
          (a : (↑(spectrum S a) : Type u_2)) → S)
        r :
      S)

Tactic:
simp [((h a).mp ha).2.left_inv _]

Premises used: And.right, Iff.mp, QuasispectrumRestricts.left_inv
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
hφ₁ : Continuous[_, inst_18] (⇑(starAlgHom (cfcHom (p := q) hqa) h) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
hφ₂ :
  (starAlgHom (cfcHom (p := q) hqa) h : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    a
⊢ Eq (α := C((↑(spectrum R a) : Type u_1), R) →⋆ₐ[R] A) (cfcHom (p := p) hpa) (starAlgHom (cfcHom (p := q) hqa) h)

Tactic:
apply cfcHom_eq_of_continuous_of_map_id

Premises used: cfcHom_eq_of_continuous_of_map_id
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ Continuous[_, inst_18] (⇑(starAlgHom (cfcHom (p := q) hqa) h) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
h.continuous_starAlgHom (cfcHom_continuous hqa)

Premises used: cfcHom_continuous, SpectrumRestricts.continuous_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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ Continuous[_, inst_18] (⇑(starAlgHom (cfcHom (p := q) hqa) h) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
exact h.continuous_starAlgHom (cfcHom_continuous hqa)

Premises used: cfcHom_continuous, SpectrumRestricts.continuous_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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ (starAlgHom (cfcHom (p := q) hqa) h : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    a

Tactic:
h.starAlgHom_id (cfcHom_id hqa)

Premises used: cfcHom_id, SpectrumRestricts.starAlgHom_id
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ (starAlgHom (cfcHom (p := q) hqa) h : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    a

Tactic:
exact h.starAlgHom_id (cfcHom_id hqa)

Premises used: cfcHom_id, SpectrumRestricts.starAlgHom_id
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
pos :
  ∀ (hg : ContinuousOn g (spectrum R a)),
    cfc (p := p) g a = cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
neg :
  ∀ (hg : ¬ContinuousOn g (spectrum R a)),
    cfc (p := p) g a = cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
⊢ cfc (p := p) g a = cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a

Tactic:
by_cases hg : ContinuousOn g (spectrum R a)

Premises used: spectrum, ContinuousOn
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ContinuousOn g (spectrum R a)
apply :
  ∀ (x : S) (hx : x ∈ spectrum S a),
    Eq (α := S)
      (Function.extend (α := { x : S // x ∈ spectrum S a }) (Subtype.val (p := fun (x : S) ↦ x ∈ spectrum S a))
          (⇑(ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
                ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
                      C((↑(spectrum R a) : Type u_1), R) }.comp
                  {
                    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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) })) :
            (a : (↑(spectrum S a) : Type u_2)) → S)
          0 x :
        S)
      ((algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x)) : S)
⊢ cfc.{u_2, u_3} (R := S) (p := q)
      (Function.extend (α := { x : S // x ∈ spectrum S a }) (Subtype.val (p := fun (x : S) ↦ x ∈ spectrum S a))
        (⇑(ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(R, S) }
              ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
                    C((↑(spectrum R a) : Type u_1), R) }.comp
                {
                  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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) })) :
          (a : (↑(spectrum S a) : Type u_2)) → S)
        0)
      a =
    cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a

Tactic:
apply cfc_congr fun x hx ↦ ?_

Premises used: cfc_congr
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ContinuousOn g (spectrum R a)
x : S
hx : x ∈ spectrum S a
⊢ x ∈ spectrum S a

Tactic:
hx
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ContinuousOn g (spectrum R a)
x : S
hx : x ∈ spectrum S a
lift :
  ∀ (x : { x : S // x ∈ spectrum S a }),
    Eq (α := S)
      (Function.extend (α := { x : S // x ∈ spectrum S a }) (Subtype.val (p := fun (x : S) ↦ x ∈ spectrum S a))
          (⇑(ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
                ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
                      C((↑(spectrum R a) : Type u_1), R) }.comp
                  {
                    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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) })) :
            (a : (↑(spectrum S a) : Type u_2)) → S)
          0 (↑x : S) :
        S)
      ((algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) (↑x : S))) : S)
⊢ Eq (α := S)
    (Function.extend (α := { x : S // x ∈ spectrum S a }) (Subtype.val (p := fun (x : S) ↦ x ∈ spectrum S a))
        (⇑(ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
              ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
                    C((↑(spectrum R a) : Type u_1), R) }.comp
                {
                  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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) })) :
          (a : (↑(spectrum S a) : Type u_2)) → S)
        0 x :
      S)
    ((algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x)) : S)

Tactic:
lift x to spectrum S a using hx

Premises used: spectrum
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ContinuousOn g (spectrum R a)
x : { x : S // x ∈ spectrum S a }
⊢ Eq (α := S)
    (Function.extend (α := { x : S // x ∈ spectrum S a }) (Subtype.val (p := fun (x : S) ↦ x ∈ spectrum S a))
        (⇑(ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
              ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
                    C((↑(spectrum R a) : Type u_1), R) }.comp
                {
                  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.{u_2, u_1} (↑(spectrum S a) : Type u_2) (↑(spectrum R a) : Type u_1) })) :
          (a : (↑(spectrum S a) : Type u_2)) → S)
        0 (↑x : S) :
      S)
    ((algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) (↑x : S))) : S)

Tactic:
simp [Function.comp]

Premises used: Function.comp
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬ContinuousOn g (spectrum R a)
⊢ ¬ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (spectrum S a)

Tactic:
fun hg' ↦ hg ?_

Premises used: Not
-- 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
inst_20 : ContinuousFunctionalCalculus R A p
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
g : R → R
hg : ¬ContinuousOn g (spectrum R a)
refine :
  ∀
    (hg' :
      ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (spectrum S a)),
    ContinuousOn g (spectrum R a)
⊢ ¬ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (spectrum S a)

Tactic:
refine fun hg' ↦ hg ?_