case h₁
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ desc inl inr = inl ≫ 𝟙 (X ⨿ Y)

case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ desc inl inr = 𝟙 (X ⨿ Y)
apply coprod.hom_ext
case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)
case h₁
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ desc inl inr = inl ≫ 𝟙 (X ⨿ Y)

case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)
simp
no goals
case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)
simp