-- 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 := ⋯ }
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((↑(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 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) 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)))
  (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)))
Tactic: simp_rw +instances [← isUniformEmbedding_toContinuousMap.comap_uniformity, this,
    @inf_uniformity _ (.comap _ _) (.comap _ _), uniformity_comap, Filter.comap_inf,
    Filter.comap_comap]