-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
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)
simp_rw :
  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)))
    (Filter.comap (β := C((↑(spectrum R a) : Type u_1), R) × C((↑(spectrum R a) : Type u_1), 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 f) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦
            x.comp f)
          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((↑(spectrum 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)))
⊢ 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)₀)

Tactic:
simp_rw +instances [← isUniformEmbedding_toContinuousMap.comap_uniformity, this,
    @inf_uniformity _ (.comap _ _) (.comap _ _), uniformity_comap, Filter.comap_inf,
    Filter.comap_comap]

Premises used: IsUniformInducing.comap_uniformity, IsUniformEmbedding.toIsUniformInducing, Filter.comap_inf, Filter.comap_comap, inf_uniformity, ContinuousMapZero.isUniformEmbedding_toContinuousMap, uniformity_comap