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 : 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 : CompleteSpace R
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
hφ :
  IsClosedEmbedding.{u_2, u_3} (X := C((↑(σₙ S a) : Type u_2), S)₀) (Y := 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 : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Eq.{u_2 + 1} (α := (↑(σₙ S a) : Type u_2))
    ((h.homeomorph.symm : (a_1 : (↑(σₙ R a) : Type u_1)) → (↑(σₙ S a) : Type u_2)) 0) 0

Tactic:
have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)
-- 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
inst_21 : CompleteSpace R
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
hφ :
  IsClosedEmbedding.{u_2, u_3} (X := C((↑(σₙ S a) : Type u_2), S)₀) (Y := 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 : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this :
  Eq.{u_2 + 1} (α := (↑(σₙ S a) : Type u_2))
    ((h.homeomorph.symm : (a_1 : (↑(σₙ R a) : Type u_1)) → (↑(σₙ S a) : Type u_2)) 0) 0
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(nonUnitalStarAlgHom φ h) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
hφ.comp <| IsUniformEmbedding.isClosedEmbedding <| .comp
    (ContinuousMapZero.isUniformEmbedding_comp _ halg)
    (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.isUniformEmbedding)

Premises used: IsUniformEmbedding.comp, Topology.IsClosedEmbedding.comp, UniformEquiv.arrowCongrLeft₀, ContinuousMapZero.isUniformEmbedding_comp, Homeomorph.symm, IsUniformEmbedding.isClosedEmbedding, QuasispectrumRestricts.homeomorph, UniformEquiv.isUniformEmbedding
-- 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
inst_21 : CompleteSpace R
a : A
φ : C((↑(σₙ S a) : Type u_2), S)₀ →⋆ₙₐ[S] A
hφ :
  IsClosedEmbedding.{u_2, u_3} (X := C((↑(σₙ S a) : Type u_2), S)₀) (Y := 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 : IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this :
  Eq.{u_2 + 1} (α := (↑(σₙ S a) : Type u_2))
    ((h.homeomorph.symm : (a_1 : (↑(σₙ R a) : Type u_1)) → (↑(σₙ S a) : Type u_2)) 0) 0
⊢ IsClosedEmbedding.{u_1, u_3} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(nonUnitalStarAlgHom φ h) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
refine hφ.comp <| IsUniformEmbedding.isClosedEmbedding <| .comp
    (ContinuousMapZero.isUniformEmbedding_comp _ halg)
    (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.isUniformEmbedding)

Premises used: Topology.IsClosedEmbedding.comp, IsUniformEmbedding.isClosedEmbedding
-- 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
⊢ CompactSpace.{u_2} (↑(σₙ S a) : Type u_2)

Tactic:
have := NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum (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 : 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
this : CompactSpace.{u_2} (↑(σₙ S a) : Type u_2)
rw : ∀ (this : IsCompact (σₙ S a)), IsCompact (σₙ R a)
⊢ CompactSpace.{u_1} (↑(σₙ 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 : 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
this : IsCompact (σₙ S a)
⊢ IsCompact (σₙ 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 : 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
⊢ ∃ (φ : C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A),
    Continuous[_, inst_20] (⇑φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) ∧
      Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
          (⇑φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) ∧
        (φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
              { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
            a ∧
          (∀ (f : C((↑(σₙ R a) : Type u_1), R)₀),
              quasispectrum.{u_1, u_3} R (A := A) ((φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) =
                range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) ∧
            ∀ (f : C((↑(σₙ R a) : Type u_1), R)₀), p ((φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)

Tactic:
⟨((h a).mp ha).2.nonUnitalStarAlgHom (cfcₙHom ((h a).mp ha).1 (R := S)),
      ?hom_continuous, ?hom_injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Iff.mp, cfcₙHom, QuasispectrumRestricts.nonUnitalStarAlgHom
-- 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
refine :
  Continuous[_, inst_20] (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
refine₁ :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
refine₂ :
  (nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    a
refine₃ :
  ∀ (f_1 : C((↑(σₙ R a) : Type u_1), R)₀),
    quasispectrum.{u_1, u_3} R (A := A)
        ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f_1 : A) =
      range (ι := (↑(σₙ R a) : Type u_1)) (⇑f_1 : (a : (↑(σₙ R a) : Type u_1)) → R)
refine₄ :
  ∀ (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)
⊢ ∃ (φ : C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A),
    Continuous[_, inst_20] (⇑φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) ∧
      Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
          (⇑φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) ∧
        (φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
              { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
            a ∧
          (∀ (f : C((↑(σₙ R a) : Type u_1), R)₀),
              quasispectrum.{u_1, u_3} R (A := A) ((φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) =
                range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) ∧
            ∀ (f : C((↑(σₙ R a) : Type u_1), R)₀), p ((φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)

Tactic:
refine ⟨((h a).mp ha).2.nonUnitalStarAlgHom (cfcₙHom ((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 : 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
⊢ Continuous[_, inst_20] (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
continuous_nonUnitalStarAlgHom (cfcₙHom_continuous _) _

Premises used: QuasispectrumRestricts.continuous_nonUnitalStarAlgHom, cfcₙHom_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 : 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
⊢ Continuous[_, inst_20] (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
exact continuous_nonUnitalStarAlgHom (cfcₙHom_continuous _) _

Premises used: QuasispectrumRestricts.continuous_nonUnitalStarAlgHom, cfcₙHom_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 : 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
⊢ Continuous[_, inst_20] (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
case hom_continuous => exact continuous_nonUnitalStarAlgHom (cfcₙHom_continuous _) _

Premises used: QuasispectrumRestricts.continuous_nonUnitalStarAlgHom, cfcₙHom_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 : 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
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
nonUnitalStarAlgHom_injective (cfcₙHom_injective _) _ halg.injective

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, QuasispectrumRestricts.nonUnitalStarAlgHom_injective, cfcₙHom_injective, Topology.IsEmbedding.injective
-- 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
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
exact nonUnitalStarAlgHom_injective (cfcₙHom_injective _) _ halg.injective

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, QuasispectrumRestricts.nonUnitalStarAlgHom_injective, cfcₙHom_injective, Topology.IsEmbedding.injective
-- 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
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
case hom_injective => exact nonUnitalStarAlgHom_injective (cfcₙHom_injective _) _ halg.injective

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, QuasispectrumRestricts.nonUnitalStarAlgHom_injective, cfcₙHom_injective, Topology.IsEmbedding.injective
-- 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
⊢ (nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    a

Tactic:
((h a).mp ha).2.nonUnitalStarAlgHom_id <| cfcₙHom_id ((h a).mp ha).1

Premises used: QuasispectrumRestricts.nonUnitalStarAlgHom_id, cfcₙHom_id, ContinuousMapZero.id, 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 : 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
⊢ (nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    a

Tactic:
exact ((h a).mp ha).2.nonUnitalStarAlgHom_id <| cfcₙHom_id ((h a).mp ha).1

Premises used: QuasispectrumRestricts.nonUnitalStarAlgHom_id, cfcₙHom_id, And.right, And.left, Iff.mp