-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
s : Cone (pair M N)
⊢ Eq (α := s.pt ⟶ Functor.obj (pair M N) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y :=
        { pt := of R ((↑M : Type v) × (↑N : Type v)),
            π :=
              {
                app := fun (j : Discrete WalkingPair) ↦
                  Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                    Functor.obj
                        (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v)))) x ⟶
                      Functor.obj (pair M N) x)
                    j fun (j : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                      Functor.obj
                          (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                          { as := x : Discrete WalkingPair } ⟶
                        Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                      j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v)))
                      (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
                naturality := ⋯ :
                NatTrans (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                  (pair M N) } :
            Cone (pair M N) }.pt)
        (↟(LinearMap.prod (Hom.hom (s.π.app { as := WalkingPair.left }))
              (Hom.hom (s.π.app { as := WalkingPair.right }))) :
          Quiver.Hom (V := ModuleCat.{v, u} R) (of R (↑s.1 : Type v)) (of R ((↑M : Type v) × (↑N : Type v))))
        ({ pt := of R ((↑M : Type v) × (↑N : Type v)),
                  π :=
                    {
                      app := fun (j : Discrete WalkingPair) ↦
                        Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                          Functor.obj
                              (Functor.obj (Functor.const (Discrete WalkingPair))
                                (of R ((↑M : Type v) × (↑N : Type v))))
                              x ⟶
                            Functor.obj (pair M N) x)
                          j fun (j : WalkingPair) ↦
                          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                            Functor.obj
                                (Functor.obj (Functor.const (Discrete WalkingPair))
                                  (of R ((↑M : Type v) × (↑N : Type v))))
                                { as := x : Discrete WalkingPair } ⟶
                              Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                            j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v)))
                            (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
                      naturality := ⋯ :
                      NatTrans
                        (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                        (pair M N) } }.π.app
            { as := WalkingPair.right } :
          Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                { pt := of R ((↑M : Type v) × (↑N : Type v)),
                    π :=
                      {
                        app := fun (j : Discrete WalkingPair) ↦
                          Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                            Functor.obj
                                (Functor.obj (Functor.const (Discrete WalkingPair))
                                  (of R ((↑M : Type v) × (↑N : Type v))))
                                x ⟶
                              Functor.obj (pair M N) x)
                            j fun (j : WalkingPair) ↦
                            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                              Functor.obj
                                  (Functor.obj (Functor.const (Discrete WalkingPair))
                                    (of R ((↑M : Type v) × (↑N : Type v))))
                                  { as := x : Discrete WalkingPair } ⟶
                                Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                              j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v)))
                              (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
                        naturality := ⋯ :
                        NatTrans
                          (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                          (pair M N) } :
                    Cone (pair M N) }.pt)
              { as := WalkingPair.right : Discrete WalkingPair } ⟶
            Functor.obj (pair M N) { as := WalkingPair.right : Discrete WalkingPair }) :
      s.pt ⟶ Functor.obj (pair M N) { as := WalkingPair.right : Discrete WalkingPair })
    (s.π.app { as := WalkingPair.right } :
      Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj (pair M N) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
rfl