-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.SigmaComparison (goal)
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : PreservesFiniteProducts X
α : Type u
inst_2 : Finite α
σ : α → Type u
inst_3 : (a : α) → TopologicalSpace (σ a)
inst_4 : ∀ (a : α), CompactSpace.{u} (σ a)
inst_5 : ∀ (a : α), T2Space.{u} (σ a)
inst_6 : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (FC := TypeCat.Fun) (X.obj (∏ᶜ fun (a : α) ↦ Opposite.op (of P (σ a))))),
    Eq (α := X.obj (Opposite.op (of P (σ a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (b : α) ↦ X.obj (Opposite.op (of P (σ b)))) a) :
            (a_1 : ∏ᶜ fun (b : α) ↦ X.obj (Opposite.op (of P (σ b)))) → X.obj (Opposite.op (of P (σ a))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (piComparison X fun (a : α) ↦ Opposite.op (of P (σ a))) :
              (a : X.obj (∏ᶜ fun (a : α) ↦ Opposite.op (of P (σ a)))) →
                ∏ᶜ fun (b : α) ↦ X.obj (Opposite.op (of P (σ b))))
            x) :
        X.obj (Opposite.op (of P (σ a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Pi.π (fun (a : α) ↦ Opposite.op (of P (σ a))) a)) :
            (a_1 : X.obj (∏ᶜ fun (a : α) ↦ Opposite.op (of P (σ a)))) → X.obj (Opposite.op (of P (σ a))))
          x :
        X.obj (Opposite.op (of P (σ a))))
⊢ Eq (α := X.obj (Opposite.op (of P (σ a))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (sigmaComparison.{u, w} (P := P) X σ) :
            TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a)))) ((a : α) → X.obj (Opposite.op (of P (σ a))))) :
          (a : X.obj (Opposite.op (of P ((a : α) × σ a)))) → (a : α) → X.obj (Opposite.op (of P (σ a))))
        x a :
      X.obj (Opposite.op (of P (σ a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (a : α) ↦ X.obj (Opposite.op (of P (σ a)))) a) :
          (a_1 : ∏ᶜ fun (a : α) ↦ X.obj (Opposite.op (of P (σ a)))) → X.obj (Opposite.op (of P (σ a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (piComparison X fun (a : α) ↦ Opposite.op (of P (σ a))) :
            (a : X.obj (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x)))) → ∏ᶜ fun (j : α) ↦ X.obj (Opposite.op (of P (σ j))))
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (X.map
                    (Iso.hom
                      (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
                        (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))) :
                TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a))))
                  (X.obj (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))))) :
              (a : X.obj (Opposite.op (of P ((a : α) × σ a)))) → X.obj (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))))
            x)) :
      X.obj (Opposite.op (of P (σ a))))
have h : Eq (α := X.obj (Opposite.op (of P (σ a))))
  (((ConcreteCategory.hom (FC := TypeCat.Fun) (sigmaComparison.{u, w} (P := P) X σ) :
          TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a)))) ((a : α) → X.obj (Opposite.op (of P (σ a))))) :
        (a : X.obj (Opposite.op (of P ((a : α) × σ a)))) → (a : α) → X.obj (Opposite.op (of P (σ a))))
      x a :
    X.obj (Opposite.op (of P (σ a))))
  (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (X.map
              (CategoryStruct.comp (Y := ∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x)))
                (Iso.hom
                  (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
                    (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))
                (Pi.π (fun (a : α) ↦ Opposite.op (of P (σ a))) a))) :
          TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a)))) (X.obj (Opposite.op (of P (σ a))))) :
        (a_1 : X.obj (Opposite.op (of P ((a : α) × σ a)))) → X.obj (Opposite.op (of P (σ a))))
      x :
    X.obj (Opposite.op (of P (σ a))))
Tactic: rw [this, ← comp_apply, ← Functor.map_comp]