no goals
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
X Y : C
b : BinaryBicone X Y
i : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ (BinaryBicone.toCone b).π.app j = 𝟙 b.pt ≫ (BinaryBicone.toCone b).π.app j
rcases j with ⟨⟨⟩⟩ <;> simp