case mk.right
C : Type u₁
inst✝ : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ BinaryFan.snd c = 𝟙 c.pt ≫ BinaryFan.snd c
case mk.right
C : Type u₁
inst✝ : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.π.app { as := WalkingPair.right } =
    (Iso.refl c.pt).hom ≫
      (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app
        { as := WalkingPair.right }
dsimp
no goals
case mk.right
C : Type u₁
inst✝ : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ BinaryFan.snd c = 𝟙 c.pt ≫ BinaryFan.snd c
simp