[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ∀ ⦃X Y : Discrete WalkingPair⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map f ≫
        (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N)) Y =
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N)) X ≫
        (pair M N).map f
[PROOFSTEP]
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟨⟩⟩⟩
[GOAL]
case mk.left.mk.left.up.up.refl
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map
        { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } } ≫
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.left } =
    (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.left } ≫
      (pair M N).map { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } }
[PROOFSTEP]
rfl
[GOAL]
case mk.right.mk.right.up.up.refl
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map
        { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } } ≫
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.right } =
    (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.right } ≫
      (pair M N).map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ∀ (s : Cone (pair M N)) (j : Discrete WalkingPair),
    (fun s =>
            LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
          s ≫
        NatTrans.app
          { pt := of R (↑M × ↑N),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
          j =
      NatTrans.app s.π j
[PROOFSTEP]
rintro s (⟨⟩ | ⟨⟩)
[GOAL]
case mk.left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ (fun s => LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
        s ≫
      NatTrans.app
        { pt := of R (↑M × ↑N),
            π :=
              NatTrans.mk fun j =>
                Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
        { as := WalkingPair.left } =
    NatTrans.app s.π { as := WalkingPair.left }
[PROOFSTEP]
rfl
[GOAL]
case mk.right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ (fun s => LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
        s ≫
      NatTrans.app
        { pt := of R (↑M × ↑N),
            π :=
              NatTrans.mk fun j =>
                Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
        { as := WalkingPair.right } =
    NatTrans.app s.π { as := WalkingPair.right }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          NatTrans.mk fun j =>
            Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        NatTrans.app
          { pt := of R (↑M × ↑N),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
          j =
      NatTrans.app s.π j
⊢ m =
    (fun s =>
        LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
      s
[PROOFSTEP]
simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          NatTrans.mk fun j =>
            Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        NatTrans.app
          { pt := of R (↑M × ↑N),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
          j =
      NatTrans.app s.π j
⊢ m = LinearMap.prod (m ≫ LinearMap.fst R ↑M ↑N) (m ≫ LinearMap.snd R ↑M ↑N)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.pt
⊢ (fun x j => ↑(NatTrans.app s.π { as := j }) x) (x + y) =
    (fun x j => ↑(NatTrans.app s.π { as := j }) x) x + (fun x j => ↑(NatTrans.app s.π { as := j }) x) y
[PROOFSTEP]
simp only [Functor.const_obj_obj, map_add]
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.pt
⊢ (fun j => ↑(NatTrans.app s.π { as := j }) x + ↑(NatTrans.app s.π { as := j }) y) =
    (fun j => ↑(NatTrans.app s.π { as := j }) x) + fun j => ↑(NatTrans.app s.π { as := j }) y
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : ↑s.pt
⊢ AddHom.toFun
      { toFun := fun x j => ↑(NatTrans.app s.π { as := j }) x,
        map_add' :=
          (_ :
            ∀ (x y : ↑s.pt),
              (fun x j => ↑(NatTrans.app s.π { as := j }) x) (x + y) =
                (fun x j => ↑(NatTrans.app s.π { as := j }) x) x + (fun x j => ↑(NatTrans.app s.π { as := j }) x) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun x j => ↑(NatTrans.app s.π { as := j }) x,
          map_add' :=
            (_ :
              ∀ (x y : ↑s.pt),
                (fun x j => ↑(NatTrans.app s.π { as := j }) x) (x + y) =
                  (fun x j => ↑(NatTrans.app s.π { as := j }) x) x + (fun x j => ↑(NatTrans.app s.π { as := j }) x) y) }
        x
[PROOFSTEP]
simp only [Functor.const_obj_obj, map_smul]
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : ↑s.pt
⊢ (fun j => r • ↑(NatTrans.app s.π { as := j }) x) = ↑(RingHom.id R) r • fun j => ↑(NatTrans.app s.π { as := j }) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫ NatTrans.app { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π j =
      NatTrans.app s.π j
⊢ m = lift f s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫ NatTrans.app { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π j =
      NatTrans.app s.π j
x : ↑s.pt
⊢ ↑m x = ↑(lift f s) x
[PROOFSTEP]
funext j
[GOAL]
case h.h
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫ NatTrans.app { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π j =
      NatTrans.app s.π j
x : ↑s.pt
j : J
⊢ ↑m x j = ↑(lift f s) x j
[PROOFSTEP]
exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)
