J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ prodFst = BinaryFan.fst (prodBinaryFan X Y)
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ (prodIsoProd X Y).hom ≫ prodFst = prod.fst
simp [← Iso.eq_inv_comp, prodIsoProd]
no goals
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ prodFst = BinaryFan.fst (prodBinaryFan X Y)
rfl