-- Mathlib/Topology/Category/TopCat/Yoneda.lean
theorem piComparison_fac {α : Type} (X : α → TopCat) :
    piComparison (yonedaPresheaf'.{w, w'} Y) (fun x ↦ op (X x)) =
    (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
    (equivEquivIso (sigmaEquiv Y (fun x ↦ (X x).1))).inv ≫ (Types.productIso _).inv

Proof state:
case h.h.h
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
a✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x => op (X x))
x✝ : α
a✝ : ↑(X x✝)
⊢ (((piComparison (yonedaPresheaf' Y) fun x => op (X x)) ≫ (Types.productIso fun i => C(↑(X i), Y)).hom) a✝¹ x✝) a✝ =
    (((yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
          (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv)
        a✝¹ x✝)
      a✝

Tactic:
simp only [yonedaPresheaf', unop_op, piComparison, types_comp_apply,
  Types.productIso_hom_comp_eval_apply, Types.pi_lift_π_apply, comp_apply, TopCat.coe_of,
  unop_comp, Quiver.Hom.unop_op, sigmaEquiv, equivEquivIso_hom, Equiv.toIso_inv,
  Equiv.coe_fn_symm_mk, comp_assoc, sigmaMk_apply, ← opCoproductIsoProduct_inv_comp_ι]

Result:
case h.h.h
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
a✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x => op (X x))
x✝ : α
a✝ : ↑(X x✝)
⊢ a✝¹ ((TopCat.Hom.hom (Sigma.ι X x✝ ≫ (opCoproductIsoProduct X).inv.unop)) a✝) =
    a✝¹ ((TopCat.Hom.hom ((TopCat.sigmaIsoSigma X).inv ≫ (opCoproductIsoProduct X).inv.unop)) ⟨x✝, a✝⟩)

Proof state:
case h.h.h
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
a✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x => op (X x))
x✝ : α
a✝ : ↑(X x✝)
⊢ a✝¹ ((TopCat.Hom.hom (Sigma.ι X x✝ ≫ (opCoproductIsoProduct X).inv.unop)) a✝) =
    a✝¹ ((TopCat.Hom.hom ((TopCat.sigmaIsoSigma X).inv ≫ (opCoproductIsoProduct X).inv.unop)) ⟨x✝, a✝⟩)

Tactic:
rfl

Result:
no goals

Proof state:
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun x => op (X x)) ≫ (Types.productIso fun i => C(↑(X i), Y)).hom =
    (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv

Tactic:
ext

Result:
case h.h.h
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
a✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x => op (X x))
x✝ : α
a✝ : ↑(X x✝)
⊢ (((piComparison (yonedaPresheaf' Y) fun x => op (X x)) ≫ (Types.productIso fun i => C(↑(X i), Y)).hom) a✝¹ x✝) a✝ =
    (((yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
          (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv)
        a✝¹ x✝)
      a✝

Proof state:
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun x => op (X x)) =
    (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv ≫ (Types.productIso fun i => C(↑(X i), Y)).inv

Tactic:
rw [← Category.assoc, Iso.eq_comp_inv]

Result:
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun x => op (X x)) ≫ (Types.productIso fun i => C(↑(X i), Y)).hom =
    (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv