-- 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.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

Tactic:
simp only [opCoproductIsoProduct, ← unop_comp, opCoproductIsoProduct'_comp_self]

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 ≫
      ((finiteCoproduct.isColimit fun a => of P (σ a)).coconePointUniqueUpToIso
              (coproductIsCoproduct fun a => of P (σ a))).op.inv.unop

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 =
    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:
simp only [sigmaComparison]

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
⊢ 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

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 := ⋯ } = (finiteCoproduct.cofan fun a => of P (σ a)).ι.app { as := a }

Tactic:
rfl

Result:
no goals

Proof state:
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)
⊢ sigmaComparison X σ =
    (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

Tactic:
ext x 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 : α
⊢ 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