no goals
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0
simp
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι.app j ≫ (fun s => 0) s = s.ι.app j
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι.app j ≫ (fun s => 0) s = s.ι.app j
have c :=
  @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _) (by simp)
    (by simpa using PushoutCocone.condition s)
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι.app j ≫ (fun s => 0) s = s.ι.app j
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι.app j ≫ (fun s => 0) s = s.ι.app j
dsimp at c
no goals
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι.app j ≫ (fun s => 0) s = s.ι.app j
simpa using c
no goals
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inl s ≫ 0 = PushoutCocone.inl s ≫ 𝟙 s.pt
simp
no goals
C : Type u₁
inst✝² : Category C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inr s ≫ 0 = PushoutCocone.inr s ≫ 𝟙 s.pt
simpa using PushoutCocone.condition s