[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map f ≫ F.map π = F.map g ≫ F.map π
[PROOFSTEP]
rw [← F.map_comp, q.condition, F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)
[PROOFSTEP]
rw [← F.map_comp, q.rightSection_π, F.map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.leftSection ≫ F.map g = 𝟙 (F.obj Y)
[PROOFSTEP]
rw [← F.map_comp, q.leftSection_bottom, F.map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection
[PROOFSTEP]
rw [← F.map_comp, q.leftSection_top, F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ Cofork.π (asCofork t) ≫ t.rightSection ≫ Cofork.π s = Cofork.π s
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ h ≫ t.rightSection ≫ Cofork.π s = Cofork.π s
[PROOFSTEP]
rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj (asCofork t).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (asCofork t) ≫ m✝ = Cofork.π s
⊢ m✝ = t.rightSection ≫ Cofork.π s
[PROOFSTEP]
simp [← hm]
