-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
H : Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ))) (𝓤 (α →ᵤ[𝔖] β × γ)) (𝓤 (α →ᵤ[𝔖] β × γ))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)))
    (comap (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
        ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.1, p.2.1)) ∘
          fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
          ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.1,
            (Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap (β := (α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ))
        ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.2, p.2.2)) ∘
          fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
          ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.1,
            (Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)))
    (𝓤 (α →ᵤ[𝔖] β × γ))
have h : Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)))
  (comap (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
      ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.1, p.2.1)) ∘
        fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
        ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.1,
          (Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.2))
      (𝓤 (α →ᵤ[𝔖] β)) ⊓
    comap (β := (α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ))
      ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.2, p.2.2)) ∘
        fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
        ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.1,
          (Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.2))
      (𝓤 (α →ᵤ[𝔖] γ)))
  (𝓤 (α →ᵤ[𝔖] β × γ))
Tactic: rw [UniformOnFun.comap_eq, UniformOnFun.comap_eq]