-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma isClosedEmbedding_cfcₙHom_of_cfcHom {a : A} (ha : p a) :
    IsClosedEmbedding (cfcₙHom_of_cfcHom R ha)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this :
  inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) =
    UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance
⊢ Filter.comap
      ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘
        Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap)
      (𝓤 C(Unit, R)) =
    ⊤

Tactic:
have : ∀ U ∈ 𝓤 (C(Unit, R)), (0, 0) ∈ U := fun U hU ↦ refl_mem_uniformity hU

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) =
    UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
⊢ Filter.comap
      ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘
        Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap)
      (𝓤 C(Unit, R)) =
    ⊤

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) =
    UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
⊢ Filter.comap
      ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘
        Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap)
      (𝓤 C(Unit, R)) =
    ⊤

Tactic:
convert Filter.comap_const_of_mem this with ⟨u, v⟩ <;>
ext ⟨x, rfl⟩ <;> [exact map_zero u; exact map_zero v]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ IsClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)

Tactic:
refine (cfcHom_isClosedEmbedding ha).comp <|
  (IsUniformInducing.isUniformEmbedding ⟨?_⟩).isClosedEmbedding

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ Filter.comap
      (fun x =>
        (↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.1,
          ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.2))
      (𝓤 C(↑(spectrum R a), R)) =
    𝓤 C(↑(σₙ R a), R)₀

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this :
  inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) =
    UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance
⊢ Filter.comap
      (fun x =>
        (↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.1,
          ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.2))
      (𝓤 C(↑(spectrum R a), R)) =
    Filter.comap
        ((Prod.map (fun x => x.comp f) fun x => x.comp f) ∘
          Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap)
        (𝓤 C(↑(spectrum R a), R)) ⊓
      Filter.comap
        ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘
          Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap)
        (𝓤 C(Unit, R))

Tactic:
refine .symm <| inf_eq_left.mpr <| le_top.trans <| eq_top_iff.mp ?_

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this :
  inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) =
    UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance
⊢ Filter.comap
      ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘
        Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap)
      (𝓤 C(Unit, R)) =
    ⊤