case refine'_1
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ (inl ≫ (IsLimit.conePointUniqueUpToIso hb.isLimit (BinaryBiproduct.isLimit X Y)).inv) ≫
      (BinaryBicone.toCone b).π.app j =
    (inl ≫ desc b.inl b.inr) ≫ (BinaryBicone.toCone b).π.app j

case refine'_2
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ (inr ≫ (IsLimit.conePointUniqueUpToIso hb.isLimit (BinaryBiproduct.isLimit X Y)).inv) ≫
      (BinaryBicone.toCone b).π.app j =
    (inr ≫ desc b.inl b.inr) ≫ (BinaryBicone.toCone b).π.app j
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ (IsLimit.conePointUniqueUpToIso hb.isLimit (BinaryBiproduct.isLimit X Y)).inv = desc b.inl b.inr
refine' biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => _) (hb.isLimit.hom_ext fun j => _)
case refine'_1.mk.left
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inl ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.left }

case refine'_1.mk.right
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inl ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.right }

case refine'_2.mk.left
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.left }

case refine'_2.mk.right
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.right }
case refine'_1
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ (inl ≫ (IsLimit.conePointUniqueUpToIso hb.isLimit (BinaryBiproduct.isLimit X Y)).inv) ≫
      (BinaryBicone.toCone b).π.app j =
    (inl ≫ desc b.inl b.inr) ≫ (BinaryBicone.toCone b).π.app j

case refine'_2
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ (inr ≫ (IsLimit.conePointUniqueUpToIso hb.isLimit (BinaryBiproduct.isLimit X Y)).inv) ≫
      (BinaryBicone.toCone b).π.app j =
    (inr ≫ desc b.inl b.inr) ≫ (BinaryBicone.toCone b).π.app j
all_goals
  simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
  rcases j with ⟨⟨⟩⟩
no goals
case refine'_1.mk.left
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inl ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.left }

case refine'_1.mk.right
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inl ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.right }

case refine'_2.mk.left
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.left }

case refine'_2.mk.right
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.right }
all_goals simp
case refine'_2
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app j =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app j
case refine'_2
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ (inr ≫ (IsLimit.conePointUniqueUpToIso hb.isLimit (BinaryBiproduct.isLimit X Y)).inv) ≫
      (BinaryBicone.toCone b).π.app j =
    (inr ≫ desc b.inl b.inr) ≫ (BinaryBicone.toCone b).π.app j
simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
case refine'_2.mk.left
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.left }

case refine'_2.mk.right
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.right }
case refine'_2
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app j =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app j
rcases j with ⟨⟨⟩⟩
no goals
case refine'_2.mk.right
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ inr ≫ (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)).π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ (BinaryBicone.toCone b).π.app { as := WalkingPair.right }
simp