-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
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 ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ))) (𝓤 (α →ᵤ[𝔖] β × γ)) (𝓤 (α →ᵤ[𝔖] β × γ))
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))
        (𝓤 (α →ᵤ[𝔖] γ)))
    (𝓤 (α →ᵤ[𝔖] β × γ))
⊢ 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]

Premises used: UniformOnFun.comap_eq