-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.conePointUniqueUpToIso_inv (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y}
    (hb : b.IsBilimit) :
    (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit _ _)).inv =
      biprod.desc b.inl b.inr

Proof state:
case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app j = inr ≫ desc b.inl b.inr ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Result:
case refine_2.mk.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_2.mk.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

Proof state:
case refine_1.mk.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_1.mk.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

case refine_2.mk.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_2.mk.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
all_goals simp

Result:
no goals

Proof state:
case refine_1
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inl ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inl ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inr ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inr ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

Tactic:
all_goals
  simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
  rcases j with ⟨⟨⟩⟩

Result:
case refine_1.mk.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_1.mk.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

case refine_2.mk.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_2.mk.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

Proof state:
case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inr ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inr ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

Tactic:
simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]

Result:
case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app j = inr ≫ desc b.inl b.inr ≫ b.toCone.π.app j

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv = desc b.inl b.inr

Tactic:
refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)

Result:
case refine_1
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inl ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inl ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inr ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inr ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

Proof state:
case refine_2.mk.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
simp

Result:
no goals