case mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
t : Cofork f✝ g
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝, ι := ι✝ } ⟶ t
⊢ Cofork.π { pt := pt✝, ι := ι✝ } ≫ f.Hom = Cofork.π t
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
s t : Cofork f✝ g
f : s ⟶ t
⊢ Cofork.π s ≫ f.Hom = Cofork.π t
cases s
case mk.mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝¹, ι := ι✝¹ } ⟶ { pt := pt✝, ι := ι✝ }
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ f.Hom = Cofork.π { pt := pt✝, ι := ι✝ }
case mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
t : Cofork f✝ g
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝, ι := ι✝ } ⟶ t
⊢ Cofork.π { pt := pt✝, ι := ι✝ } ≫ f.Hom = Cofork.π t
cases t
case mk.mk.mk
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝
Hom✝ : { pt := pt✝¹, ι := ι✝¹ }.pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), { pt := pt✝¹, ι := ι✝¹ }.ι.app j ≫ Hom✝ = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ (CoconeMorphism.mk Hom✝).Hom = Cofork.π { pt := pt✝, ι := ι✝ }
case mk.mk
C : Type u
inst✝ : Category C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝¹, ι := ι✝¹ } ⟶ { pt := pt✝, ι := ι✝ }
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ f.Hom = Cofork.π { 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
ι✝¹ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝
Hom✝ : { pt := pt✝¹, ι := ι✝¹ }.pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), { pt := pt✝¹, ι := ι✝¹ }.ι.app j ≫ Hom✝ = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ (CoconeMorphism.mk Hom✝).Hom = Cofork.π { pt := pt✝, ι := ι✝ }
aesop