-- 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_1 :
  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)
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
h :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).1
      0
h₁ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).2
      0
h₂ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).1
      0
h₃ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).2
      0
h₄ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).1
      0
h₅ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).2
      0
h₆ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).1
      0
h₇ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
          (u, v)).2
      0
h₈ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
                (u, v)).1 :
            (a : Unit) → R)
          PUnit.unit :
        R)
      ((0 : (a : Unit) → R) PUnit.unit : R)
h₉ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
                (u, v)).2 :
            (a : Unit) → R)
          PUnit.unit :
        R)
      ((0 : (a : Unit) → R) PUnit.unit : R)
h₁₀ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
                (u, v)).1 :
            (a : Unit) → R)
          PUnit.unit :
        R)
      ((0 : (a : Unit) → R) PUnit.unit : R)
h₁₁ :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := 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))))
                (u, v)).2 :
            (a : Unit) → R)
          PUnit.unit :
        R)
      ((0 : (a : Unit) → R) PUnit.unit : R)
⊢ 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)))
    ⊤

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

Premises used: Filter.comap_const_of_mem, rfl