case h₁
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ fst = 𝟙 (X ⨯ Y) ≫ fst

case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨯ Y)
apply prod.hom_ext
case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
case h₁
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ fst = 𝟙 (X ⨯ Y) ≫ fst

case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
simp
no goals
case h₂
C : Type u
inst✝¹ : Category C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
simp