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
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)
hg' : ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (spectrum S a)
rw : ContinuousOn.{u_1, u_2} (Y := S) ((⇑(algebraMap R S) : (a : R) → S) ∘ g) (spectrum R a)
⊢ ContinuousOn g (spectrum R a)

Tactic:
rw [halg.isEmbedding.continuousOn_iff]

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.continuousOn_iff
-- 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)
hg' : ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (spectrum S a)
⊢ ContinuousOn.{u_1, u_2} (Y := S) ((⇑(algebraMap R S) : (a : R) → S) ∘ g) (spectrum R a)

Tactic:
simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
        hg'.comp halg.isEmbedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S)

Premises used: Continuous.continuousOn, Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.continuousOn_iff, ContinuousOn.comp, Function.comp_def, spectrum.algebraMap_mem, QuasispectrumRestricts.left_inv, Topology.IsEmbedding.continuous
-- 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:
have : ¬ ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (spectrum S a) := by
      refine fun hg' ↦ hg ?_
      rw [halg.isEmbedding.continuousOn_iff]
      simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
        hg'.comp halg.isEmbedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S)
-- 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)
this : ¬ContinuousOn (Y := S) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) (spectrum S a)
neg : 0 = cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
neg₁ neg₂ : Eq.{u_3 + 1} (α := A) 0 0
⊢ 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:
rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn a this]

Premises used: cfc_apply_of_not_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 : ClosedEmbeddingContinuousFunctionalCalculus S A q
inst_20 : ContinuousMap.UniqueHom R A
inst_21 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := 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
⊢ ContinuousFunctionalCalculus R A p

Tactic:
have := SpectrumRestricts.cfc f halg.isClosedEmbedding h0 h
-- 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 : ClosedEmbeddingContinuousFunctionalCalculus S A q
inst_20 : ContinuousMap.UniqueHom R A
inst_21 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := 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
this : ContinuousFunctionalCalculus R A p
rw :
  IsClosedEmbedding.{u_1, u_3} (X := C((↑(spectrum R a) : Type u_1), R)) (Y := A)
    (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(spectrum R a) : Type u_1), R)) (Y := A)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
rw [cfcHom_eq_restrict f ha ((h a).mp ha).1 ((h a).mp ha).2]

Premises used: SpectrumRestricts.cfcHom_eq_restrict, 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 : ClosedEmbeddingContinuousFunctionalCalculus S A q
inst_20 : ContinuousMap.UniqueHom R A
inst_21 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := 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
this : ContinuousFunctionalCalculus R A p
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(spectrum R a) : Type u_1), R)) (Y := A)
    (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
isClosedEmbedding_starAlgHom (cfcHom_isClosedEmbedding ((h a).mp ha).1)
      ((h a).mp ha).2 halg

Premises used: cfcHom_isClosedEmbedding, SpectrumRestricts.isClosedEmbedding_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 : ClosedEmbeddingContinuousFunctionalCalculus S A q
inst_20 : ContinuousMap.UniqueHom R A
inst_21 : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding.{u_1, u_2} (α := R) (β := 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
this : ContinuousFunctionalCalculus R A p
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(spectrum R a) : Type u_1), R)) (Y := A)
    (⇑(starAlgHom (cfcHom (p := q) ⋯) ⋯) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
exact isClosedEmbedding_starAlgHom (cfcHom_isClosedEmbedding ((h a).mp ha).1)
      ((h a).mp ha).2 halg

Premises used: cfcHom_isClosedEmbedding, SpectrumRestricts.isClosedEmbedding_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
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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id : (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A) (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) = a
simp :
  (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A)
      (comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (comp (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
          { 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' := ⋯ })) =
    a
⊢ (nonUnitalStarAlgHom φ h : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) =
    a

Tactic:
simp only [QuasispectrumRestricts.nonUnitalStarAlgHom_apply]

Premises used: QuasispectrumRestricts.nonUnitalStarAlgHom_apply
-- 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 : 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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id : (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A) (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) = a
⊢ (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A) (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) = a

Tactic:
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 : 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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id : (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A) (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) = a
h₁ :
  Eq (α := C((↑(σₙ S a) : Type u_2), S)₀)
    (comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (comp (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
          { 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' := ⋯ }) :
      C((↑(σₙ S a) : Type u_2), S)₀)
    (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀)
⊢ (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A)
      (comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (comp (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
          { 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' := ⋯ })) =
    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 : 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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id : (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A) (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) = a
h₁ :
  ∀ (x : (↑(σₙ S a) : Type u_2)),
    Eq (α := S)
      ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
              (comp (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
                {
                  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' := ⋯ }) :
            (a : (↑(σₙ S a) : Type u_2)) → S)
          x :
        S)
      (((ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) : (a : (↑(σₙ S a) : Type u_2)) → S) x : S)
⊢ Eq (α := C((↑(σₙ S a) : Type u_2), S)₀)
    (comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (comp (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
          { 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' := ⋯ }) :
      C((↑(σₙ S a) : Type u_2), S)₀)
    (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), 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 : 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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id : (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A) (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) = a
x : (↑(σₙ S a) : Type u_2)
⊢ Eq (α := S)
    ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
            (comp (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
              {
                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' := ⋯ }) :
          (a : (↑(σₙ S a) : Type u_2)) → S)
        x :
      S)
    (((ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) : (a : (↑(σₙ S a) : Type u_2)) → S) x : S)

Tactic:
h.rightInvOn x.2

Premises used: QuasispectrumRestricts.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 : 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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id : (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A) (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) = a
x : (↑(σₙ S a) : Type u_2)
⊢ Eq (α := S)
    ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
            (comp (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
              {
                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' := ⋯ }) :
          (a : (↑(σₙ S a) : Type u_2)) → S)
        x :
      S)
    (((ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀) : (a : (↑(σₙ S a) : Type u_2)) → S) x : S)

Tactic:
exact h.rightInvOn x.2

Premises used: QuasispectrumRestricts.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 : 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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
hφ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := C((↑(σₙ S a) : Type u_2), S)₀) (β := A)
    (⇑φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A)
f : C(S, R)
h : QuasispectrumRestricts.{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((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(nonUnitalStarAlgHom φ h) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)
  hφ.comp <|
    (postcomp_injective ⟨⟨(StarAlgHom.ofId R S), (algebraMapCLM R S).continuous⟩, _⟩ halg).comp <|
    (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.injective)

Premises used: ContinuousMapZero.postcomp_injective, Algebra.algebraMap, ContinuousMap.mk, algebraMapCLM, QuasispectrumRestricts.nonUnitalStarAlgHom._proof_15, map_zero, UniformEquiv.arrowCongrLeft₀, ContinuousLinearMap.continuous, UniformEquiv.injective, Function.Injective.comp, Homeomorph.symm, ContinuousMapZero.mk, ContinuousMapZero.nonUnitalStarAlgHom_postcomp._proof_1, QuasispectrumRestricts.homeomorph, NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom, DFunLike.coe, StarAlgHom.ofId, Subtype.ext
-- 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 : 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
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
hφ : Continuous[_, inst_20] (⇑φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A)
f : C(S, R)
h : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
⊢ Continuous[_, inst_20] (⇑(nonUnitalStarAlgHom φ h) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

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

Premises used: Continuous.comp, ContinuousMapZero.continuous_postcomp, ContinuousMapZero.continuous_precomp