-- 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 : α
this :
  ∀ (a_1 : X.obj (∏ᶜ fun a => Opposite.op (of P (σ a)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ 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))

Tactic:
rw [this, ← FunctorToTypes.map_comp_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 : α
this :
  ∀ (a_1 : X.obj (∏ᶜ fun a => Opposite.op (of P (σ a)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ a))) a_1) =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ sigmaComparison X σ x a =
    X.map
      ((opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
            (productIsProduct fun x => Opposite.op (of P (σ x)))).hom ≫
        Pi.π (fun a => Opposite.op (of P (σ a))) a)
      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 : α
this :
  ∀ (a_1 : X.obj (∏ᶜ fun a => Opposite.op (of P (σ a)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ a))) a_1) =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ X.map (ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ }).op x =
    X.map
      ((opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
            (productIsProduct fun x => Opposite.op (of P (σ x)))).hom ≫
        Pi.π (fun a => Opposite.op (of P (σ a))) a)
      x

Tactic:
apply congrFun

Result:
case h.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)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ a))) a_1) =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ X.map (ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ }).op =
    X.map
      ((opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
            (productIsProduct fun x => Opposite.op (of P (σ x)))).hom ≫
        Pi.π (fun a => Opposite.op (of P (σ a))) a)

Proof state:
case h.h.h.e_a.e_f
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)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ a))) a_1) =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } =
    Sigma.ι (fun a => of P (σ a)) a ≫
      ((finiteCoproduct.isColimit fun a => of P (σ a)).coconePointUniqueUpToIso
              (coproductIsCoproduct fun a => of P (σ a))).op.inv.unop

Tactic:
erw [IsColimit.fac]

Result:
case h.h.h.e_a.e_f
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)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ a))) a_1) =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } = (finiteCoproduct.cofan fun a => of P (σ a)).ι.app { as := a }

Proof state:
case h.h.h.e_a.e_f
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)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ a))) a_1) =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } =
    ((opCoproductIsoProduct fun a => of P (σ a)).inv ≫ (Sigma.ι (fun a => of P (σ a)) a).op).unop ≫
      (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
            (productIsProduct fun x => Opposite.op (of P (σ x)))).hom.unop

Tactic:
simp only [coe_of, Opposite.unop_op, unop_comp, Quiver.Hom.unop_op, Category.assoc]

Result:
case h.h.h.e_a.e_f
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)))),
    Pi.π (fun b => X.obj (Opposite.op (of P (σ b)))) a (piComparison X (fun a => Opposite.op (of P (σ a))) a_1) =
      X.map (Pi.π (fun a => Opposite.op (of P (σ a))) a) a_1
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } =
    Sigma.ι (fun a => of P (σ a)) a ≫
      (opCoproductIsoProduct fun a => of P (σ a)).inv.unop ≫
        (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a => of P (σ a))
              (productIsProduct fun x => Opposite.op (of P (σ x)))).hom.unop