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

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

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