-- Mathlib/Topology/Category/CompHausLike/SigmaComparison.lean
theorem sigmaComparison_eq_comp_isos : sigmaComparison X σ =
    (X.mapIso (opCoproductIsoProduct'
      (finiteCoproduct.isColimit.{u, u} (fun a ↦ of P (σ a)))
      (productIsProduct fun x ↦ Opposite.op (of P (σ x))))).hom ≫
    (PreservesProduct.iso X fun a ↦ ⟨of P (σ a)⟩).hom ≫
    (Types.productIso.{u, max u w} fun a ↦ X.obj ⟨of P (σ a)⟩).hom

Proof state:
case h.h
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
⊢ sigmaComparison X σ x a =
    ((X.mapIso
            (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
              (productIsProduct fun x => Opposite.op (of P (σ x))))).hom ≫
        (PreservesProduct.iso X fun a => Opposite.op (of P (σ a))).hom ≫
          (Types.productIso fun a => X.obj (Opposite.op (of P (σ a)))).hom)
      x a

Tactic:
simp only [Cofan.mk_pt, Fan.mk_pt, Functor.mapIso_hom,
  PreservesProduct.iso_hom, types_comp_apply, Types.productIso_hom_comp_eval_apply]

Result:
case h.h
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
⊢ sigmaComparison X σ x a =
    Pi.π (fun a => X.obj (Opposite.op (of P (σ a)))) a
      (piComparison X (fun a => Opposite.op (of P (σ a)))
        (X.map
          (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
              (productIsProduct fun x => Opposite.op (of P (σ x)))).hom
          x))

Proof state:
case h.h
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
⊢ sigmaComparison X σ x a =
    Pi.π (fun a => X.obj (Opposite.op (of P (σ a)))) a
      (piComparison X (fun a => Opposite.op (of P (σ a)))
        (X.map
          (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
              (productIsProduct fun x => Opposite.op (of P (σ x)))).hom
          x))

Tactic:
have := congrFun (piComparison_comp_π X (fun a ↦ ⟨of P (σ a)⟩) a)

Result:
case h.h
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (a_1 : X.obj (∏ᶜ fun a => Opposite.op (of P (σ a)))),
    ((piComparison X fun a => Opposite.op (of P (σ a))) ≫ Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a) a_1 =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ sigmaComparison X σ x a =
    Pi.π (fun a => X.obj (Opposite.op (of P (σ a)))) a
      (piComparison X (fun a => Opposite.op (of P (σ a)))
        (X.map
          (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
              (productIsProduct fun x => Opposite.op (of P (σ x)))).hom
          x))