case x
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
X Y : C
t : BinaryBicone X Y
ht : IsLimit (BinaryBicone.toCone t)
⊢ ∀ (j : Discrete WalkingPair), t.inl ≫ (BinaryBicone.toCone t).π.app j = (BinaryFan.mk (𝟙 X) 0).π.app j
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
X Y : C
t : BinaryBicone X Y
ht : IsLimit (BinaryBicone.toCone t)
⊢ t.inl = IsLimit.lift ht (BinaryFan.mk (𝟙 X) 0)
apply ht.uniq (BinaryFan.mk (𝟙 X) 0)
no goals
case x
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
X Y : C
t : BinaryBicone X Y
ht : IsLimit (BinaryBicone.toCone t)
⊢ ∀ (j : Discrete WalkingPair), t.inl ≫ (BinaryBicone.toCone t).π.app j = (BinaryFan.mk (𝟙 X) 0).π.app j
rintro ⟨⟨⟩⟩ <;> dsimp <;> simp