case h₁
C : Type u
inst✝² : Category C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inl ≫ map h k ≫ desc f g = inl ≫ desc (h ≫ f) (k ≫ g)

case h₂
C : Type u
inst✝² : Category C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)
C : Type u
inst✝² : Category C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ map h k ≫ desc f g = desc (h ≫ f) (k ≫ g)
apply coprod.hom_ext
case h₂
C : Type u
inst✝² : Category C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)
case h₁
C : Type u
inst✝² : Category C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inl ≫ map h k ≫ desc f g = inl ≫ desc (h ≫ f) (k ≫ g)

case h₂
C : Type u
inst✝² : Category C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)
simp
no goals
case h₂
C : Type u
inst✝² : Category C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)
simp