case mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
t : Fork f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝, π := π✝ } ⟶ t
⊢ f.Hom ≫ ι t = ι { pt := pt✝, π := π✝ }
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
s t : Fork f✝ g
f : s ⟶ t
⊢ f.Hom ≫ ι t = ι s
cases s
case mk.mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝¹, π := π✝¹ } ⟶ { pt := pt✝, π := π✝ }
⊢ f.Hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }
case mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
t : Fork f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝, π := π✝ } ⟶ t
⊢ f.Hom ≫ ι t = ι { pt := pt✝, π := π✝ }
cases t
case mk.mk.mk
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f g
Hom✝ : { pt := pt✝¹, π := π✝¹ }.pt ⟶ { pt := pt✝, π := π✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), Hom✝ ≫ { pt := pt✝, π := π✝ }.π.app j = { pt := pt✝¹, π := π✝¹ }.π.app j
⊢ (ConeMorphism.mk Hom✝).Hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }
case mk.mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝¹, π := π✝¹ } ⟶ { pt := pt✝, π := π✝ }
⊢ f.Hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }
cases f
no goals
case mk.mk.mk
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f g
Hom✝ : { pt := pt✝¹, π := π✝¹ }.pt ⟶ { pt := pt✝, π := π✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), Hom✝ ≫ { pt := pt✝, π := π✝ }.π.app j = { pt := pt✝¹, π := π✝¹ }.π.app j
⊢ (ConeMorphism.mk Hom✝).Hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }
aesop