case x
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
X Y : C
t : BinaryBicone X Y
ht : IsColimit (BinaryBicone.toCocone t)
⊢ ∀ (j : Discrete WalkingPair), (BinaryBicone.toCocone t).ι.app j ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app j
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
X Y : C
t : BinaryBicone X Y
ht : IsColimit (BinaryBicone.toCocone t)
⊢ t.fst = IsColimit.desc ht (BinaryCofan.mk (𝟙 X) 0)
apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)
no goals
case x
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
X Y : C
t : BinaryBicone X Y
ht : IsColimit (BinaryBicone.toCocone t)
⊢ ∀ (j : Discrete WalkingPair), (BinaryBicone.toCocone t).ι.app j ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app j
rintro ⟨⟨⟩⟩ <;> dsimp <;> simp