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 : 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)
have 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)
Tactic: refine fun hg' ↦ hg ?_
-- 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 : 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 g (spectrum R a)
have rw : ContinuousOn.{u_1, u_2} (Y := S) ((⇑(algebraMap R S) : (a : R) → S) ∘ g) (spectrum R a)
Tactic: rw [halg.isEmbedding.continuousOn_iff]
-- 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 : 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)
⊢ cfc (p := p) g a = cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have this : ¬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)
-- 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 : 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)
⊢ cfc (p := p) g a = cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have neg : 0 = 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]
-- 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 : 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
⊢ cfc (p := p) g a = cfc (p := q) (fun (x : S) ↦ (algebraMap R S : (a : R) → S) (g ((f : (a : S) → R) x))) a
have neg₁ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn a this]
-- 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 : 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)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
have rw : IsClosedEmbedding.{u_1, u_3} (X := C((↑(spectrum R a) : Type u_1), R)) (Y := A)
  (⇑(starAlgHom (cfcHom (p := q) sorry) sorry) : (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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ (nonUnitalStarAlgHom φ h : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) =
    a
have simp : (φ : (a : C((↑(σₙ S a) : Type u_2), S)₀) → A)
    (comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry }
      (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) sorry,
          continuous_toFun := sorry, map_zero' := sorry })) =
  a
Tactic: simp only [QuasispectrumRestricts.nonUnitalStarAlgHom_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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)
      (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
have h₁ : Eq (α := C((↑(σₙ S a) : Type u_2), S)₀)
  (comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry }
      (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) sorry,
          continuous_toFun := sorry, map_zero' := sorry }) :
    C((↑(σₙ S a) : Type u_2), S)₀)
  (ContinuousMapZero.id (σₙ S a) : C((↑(σₙ S a) : Type u_2), S)₀)
Tactic: convert! h_id
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ 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)₀)
have h₁ : ∀ (x : (↑(σₙ S a) : Type u_2)),
  Eq (α := S)
    ((comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry }
            (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) sorry,
                continuous_toFun := sorry, map_zero' := sorry }) :
          (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: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (hypothesis)
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)
⊢ 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)
have 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
Tactic: have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)
-- 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
⊢ CompactSpace.{u_1} (↑(σₙ R a) : Type u_1)
have this : CompactSpace.{u_2} (↑(σₙ S a) : Type u_2)
Tactic: have := NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum (R := S) a
-- 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
this : CompactSpace.{u_2} (↑(σₙ S a) : Type u_2)
⊢ CompactSpace.{u_1} (↑(σₙ R a) : Type u_1)
have rw : ∀ (this : IsCompact (σₙ S a)), IsCompact (σₙ R a)
Tactic: rw [← isCompact_iff_compactSpace] at this ⊢
Cleared hypotheses: this
-- 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
⊢ ∃ (φ : 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 : Continuous[_, inst_20] (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → 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)
⊢ ∃ (φ : 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₁ : Function.Injective.{u_1 + 1, u_3 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
  (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) sorry) sorry) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → 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⟩