-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v₂, 0, u₂}
        (obj (const (Discrete WalkingPair))
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair })
    ((obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).π.app
      { as := WalkingPair.left })
    (Iso.hom
        (Iso.refl
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.left })
⊢ (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).π.app
      j =
    Iso.hom
        (Iso.refl
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app j
have right : Eq (α :=
  obj.{0, v₂, 0, u₂}
      (obj (const (Discrete WalkingPair))
        (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    obj.{0, v₂, 0, u₂}
      (pair
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.left : Discrete WalkingPair })
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.right : Discrete WalkingPair }))
      { as := WalkingPair.right : Discrete WalkingPair })
  ((obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
          (Bicone.toCone (F.mapBicone b.toBicone))).π.app
    { as := WalkingPair.right })
  (Iso.hom
      (Iso.refl
        (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).pt) ≫
    (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j