awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ Eq (α := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R))
have h : ∀ (x : R),
  Membership.mem (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      x ↔
    Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : R
⊢ Membership.mem (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      x ↔
    Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x
have h : Membership.mem (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    x →
  Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : R
h :
  Membership.mem (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      x →
    Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x
⊢ Membership.mem (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      x ↔
    Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x
have h₁ : Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x →
  Membership.mem (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry } :
                  (a_2 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_2 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have hx : (↑x : R) ∈ σₙ R a
Tactic: have hx := x.2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) ∈ σₙ R a
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have hx₁ : (↑x : R) ∈ spectrum R a ∪ {0}
Tactic: simp_rw [quasispectrum_eq_spectrum_union_zero R a] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) ∈ spectrum R a ∪ {0}
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have h : ∀ (hx : (↑x : R) ∈ spectrum R a),
  Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) ∈ spectrum R a ∪ {0}
h :
  ∀ (hx : (↑x : R) ∈ spectrum R a),
    Membership.mem (α := R) (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have h₁ : ∀ (hx : Membership.mem (γ := Set R) {0} (↑x : R)),
  Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : Membership.mem (γ := Set R) {0} (↑x : R)
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have h : Membership.mem (α := R) (γ := Set R) {0} ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : Membership.mem (γ := Set R) {0} (↑x : R)
⊢ Membership.mem (α := R) (γ := Set R) {0} ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have hx₁ : (↑x : R) = 0
Tactic: push _ ∈ _ at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) = 0
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) (0 : R)
have h : Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) (0 : R)
Tactic: rw [show x = 0 from Subtype.val_injective hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) = 0
h : Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) (0 : R)
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) (0 : R)
have h₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [show x = 0 from Subtype.val_injective hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(cfcₙHom_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
have refine : Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
  (Filter.comap (β := C((↑(spectrum R a) : Type u_1), R) × C((↑(spectrum R a) : Type u_1), R))
    (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
      (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                  (NonUnitalStarAlgHom.comp
                    (↑(compStarAlgHom' R R
                          { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry }) :
                      C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                    toContinuousMapHom)) :
              C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
            (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
          x.1,
        ((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                  (NonUnitalStarAlgHom.comp
                    (↑(compStarAlgHom' R R
                          { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry }) :
                      C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                    toContinuousMapHom)) :
              C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
            (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
          x.2))
    (𝓤 C((↑(spectrum R a) : Type u_1), R)))
  (𝓤 C((↑(σₙ R a) : Type u_1), R)₀)
Tactic: refine (cfcHom_isClosedEmbedding ha).comp <|
    (IsUniformInducing.isUniformEmbedding ⟨?_⟩).isClosedEmbedding
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
⊢ Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
    (Filter.comap (β := C((↑(spectrum R a) : Type u_1), R) × C((↑(spectrum R a) : Type u_1), R))
      (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
        (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                    (NonUnitalStarAlgHom.comp
                      (↑(compStarAlgHom' R R
                            { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                        C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                      toContinuousMapHom)) :
                C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
              (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
            x.1,
          ((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                    (NonUnitalStarAlgHom.comp
                      (↑(compStarAlgHom' R R
                            { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                        C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                      toContinuousMapHom)) :
                C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
              (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
            x.2))
      (𝓤 C((↑(spectrum R a) : Type u_1), R)))
    (𝓤 C((↑(σₙ R a) : Type u_1), R)₀)
have this : Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
  (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
      inferInstance ⊓
    UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
Tactic: have := uniformSpace_eq_inf_precomp_of_cover (β := R) f (0 : C(Unit, σₙ R a))
    (map_continuous f).isProperMap (map_continuous 0).isProperMap <| by
      simp only [← Subtype.val_injective.image_injective.eq_iff, f, ContinuousMap.coe_mk,
        ContinuousMap.coe_zero, range_zero, image_union, image_singleton,
        quasispectrum.coe_zero, ← range_comp, val_comp_inclusion, image_univ, Subtype.range_coe,
        quasispectrum_eq_spectrum_union_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
this :
  Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
    (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
        inferInstance ⊓
      UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
⊢ Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
    (Filter.comap (β := C(Unit, R) × C(Unit, R))
      (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
        ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
      (𝓤 C(Unit, R)))
    ⊤
have this₁ : ∀ (U : Set (C(Unit, R) × C(Unit, R))),
  Membership.mem (γ := Filter (C(Unit, R) × C(Unit, R))) (𝓤 C(Unit, R)) U → (0, 0) ∈ U
Tactic: have : ∀ U ∈ 𝓤 (C(Unit, R)), (0, 0) ∈ U := fun U hU ↦ refl_mem_uniformity hU