case h₁
C : Type u
inst✝² : Category C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ fst = lift (f ≫ h) (g ≫ k) ≫ fst

case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd
C : Type u
inst✝² : Category C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ map h k = lift (f ≫ h) (g ≫ k)
apply prod.hom_ext
case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd
case h₁
C : Type u
inst✝² : Category C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ fst = lift (f ≫ h) (g ≫ k) ≫ fst

case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd
simp
no goals
case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd
simp