awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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)
⊢ ∃ (φ : 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)
have refine₂ : (nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
    { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := sorry } =
  a
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⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ ∃ (φ : 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)
have refine₃ : ∀ (f_1 : C((↑(σₙ R a) : Type u_1), R)₀),
  quasispectrum.{u_1, u_3} R (A := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (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)
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⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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)
⊢ ∃ (φ : 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)
have refine₄ : ∀ (f_1 : C((↑(σₙ R a) : Type u_1), R)₀),
  p ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f_1)
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⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ ∀ (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)
have simp : ∀ (f_1 : C((↑(σₙ R a) : Type u_1), R)₀) (x : R),
  (∃ (y : (↑(σₙ S a) : Type u_2)),
      (f_1 : (a : (↑(σₙ R a) : Type u_1)) → R)
          (Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) sorry y) =
        x) ↔
    ∃ (y : (↑(σₙ R a) : Type u_1)), (f_1 : (a : (↑(σₙ R a) : Type u_1)) → R) y = x
Tactic: simp only [nonUnitalStarAlgHom_apply, ← @quasispectrum.preimage_algebraMap (R := R) S,
        cfcₙHom_map_quasispectrum, Set.ext_iff, Set.mem_preimage, Set.mem_range, comp_apply, coe_mk,
        ContinuousMap.coe_mk, StarAlgHom.ofId_apply, halg.injective.eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
g : C((↑(σₙ R a) : Type u_1), R)₀
⊢ p ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g)
have rw : q ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g) ∧
  QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
    ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) (⇑f : (a : S) → R)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
g : C((↑(σₙ R a) : Type u_1), R)₀
⊢ q ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g) ∧
    QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) (⇑f : (a : S) → R)
have refine : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
  ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) (⇑f : (a : S) → R)
Tactic: refine ⟨cfcₙHom_predicate _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
g : C((↑(σₙ R a) : Type u_1), R)₀
⊢ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
    ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) (⇑f : (a : S) → R)
have refine : ∀ (s : S)
  (hs :
    s ∈
      quasispectrum.{u_2, u_3} S (A := A)
        ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)),
  (algebraMap R S : (a : R) → S) ((f : (a : S) → R) s : R) = s
Tactic: refine { rightInvOn := fun s hs ↦ ?_, left_inv := ((h a).mp ha).2.left_inv }
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (hypothesis)
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
g : C((↑(σₙ R a) : Type u_1), R)₀
s : S
hs :
  s ∈
    quasispectrum.{u_2, u_3} S (A := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
⊢ (algebraMap R S : (a : R) → S) ((f : (a : S) → R) s : R) = s
have hs₁ : Membership.mem (γ := Set S)
  (range (ι := (↑(σₙ S a) : Type u_2))
    (⇑(comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry }
          (g.comp
            { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) sorry,
              continuous_toFun := sorry, map_zero' := sorry :
              ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) :
      (a : (↑(σₙ S a) : Type u_2)) → S))
  s
Tactic: rw [nonUnitalStarAlgHom_apply,
        cfcₙHom_map_quasispectrum] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
g : C((↑(σₙ R a) : Type u_1), R)₀
s : S
hs :
  Membership.mem (γ := Set S)
    (range (ι := (↑(σₙ S a) : Type u_2))
      (⇑(comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
            (g.comp
              {
                toFun :=
                  Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
                continuous_toFun := ⋯, map_zero' := ⋯ :
                ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) :
        (a : (↑(σₙ S a) : Type u_2)) → S))
    s
⊢ (algebraMap R S : (a : R) → S) ((f : (a : S) → R) s : R) = s
have obtain : ∀ (r : (↑(σₙ S a) : Type u_2)),
  Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((f : (a : S) → R)
            ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry }
                    (g.comp
                      {
                        toFun :=
                          Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R)
                            sorry,
                        continuous_toFun := sorry, map_zero' := sorry :
                        ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }) :
                  (a : (↑(σₙ S a) : Type u_2)) → S)
                r :
              S) :
          R) :
      S)
    ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry }
            (g.comp
              {
                toFun :=
                  Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) sorry,
                continuous_toFun := sorry, map_zero' := sorry :
                ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }) :
          (a : (↑(σₙ S a) : Type u_2)) → S)
        r :
      S)
Tactic: obtain ⟨r, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
case :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
    p ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g)
⊢ ∀ (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)
have case₁ : ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
  q ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g) ∧
    QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) (⇑f : (a : S) → R)
Tactic: case predicate_hom =>
      intro g
      rw [h]
      refine ⟨cfcₙHom_predicate _ _, ?_⟩
      refine { rightInvOn := fun s hs ↦ ?_, left_inv := ((h a).mp ha).2.left_inv }
      rw [nonUnitalStarAlgHom_apply,
        cfcₙHom_map_quasispectrum] at hs
      obtain ⟨r, rfl⟩ := hs
      simp [((h a).mp ha).2.left_inv _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : TopologicalSpace A
inst_21 : NonUnitalContinuousFunctionalCalculus S A q
inst_22 : IsScalarTower R A A
inst_23 : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding.{u_1, u_2} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
case :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
    p ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g)
case₁ :
  ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
    q ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g) ∧
      QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
        ((nonUnitalStarAlgHom (cfcₙHom (p := q) ⋯) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
        (⇑f : (a : S) → R)
⊢ ∀ (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)
have case₂ : ∀ (g : C((↑(σₙ R a) : Type u_1), R)₀),
  QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) (A := A)
    ((nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) (⇑f : (a : S) → R)
Tactic: case predicate_hom =>
      intro g
      rw [h]
      refine ⟨cfcₙHom_predicate _ _, ?_⟩
      refine { rightInvOn := fun s hs ↦ ?_, left_inv := ((h a).mp ha).2.left_inv }
      rw [nonUnitalStarAlgHom_apply,
        cfcₙHom_map_quasispectrum] at hs
      obtain ⟨r, rfl⟩ := hs
      simp [((h a).mp ha).2.left_inv _]