-- 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)
refine :
  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)))
    ⊤
⊢ 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)))

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

Premises used: Iff.mpr, eq_top_iff, le_top, inf_eq_left, Iff.mp, LE.le.trans