[GOAL]
R : Type u
inst✝ : Ring R
r : R
M N : ModuleCat R
f : M ⟶ N
⊢ (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f ≫
      (fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) N =
    (fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) M ≫
      (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f
[PROOFSTEP]
ext
[GOAL]
case w
R : Type u
inst✝ : Ring R
r : R
M N : ModuleCat R
f : M ⟶ N
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj M)
⊢ ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f ≫
          (fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) N)
      x✝ =
    ↑((fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) M ≫
          (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f)
      x✝
[PROOFSTEP]
exact (f.map_smul _ _).symm
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Function.LeftInverse (fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) fun r =>
    NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)
[PROOFSTEP]
intro r
[GOAL]
R : Type u
inst✝ : Ring R
r : R
⊢ (fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1)
      ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) r) =
    r
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Function.RightInverse (fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) fun r =>
    NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)
[PROOFSTEP]
intro φ
[GOAL]
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
⊢ (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
    φ
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
⊢ ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
        ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ)).app =
    φ.app
[PROOFSTEP]
ext M (x : M)
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
M : ModuleCat R
x : ↑M
⊢ ↑(NatTrans.app
          ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
            ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ))
          M)
      x =
    ↑(NatTrans.app φ M) x
[PROOFSTEP]
have w :=
  congr_fun ((forget _).congr_map (φ.naturality (ModuleCat.asHomRight (LinearMap.toSpanSingleton R M x)))) (1 : R)
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
M : ModuleCat R
x : ↑M
w :
  (forget AddCommGroupCat).map
      ((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map
          (ModuleCat.asHomRight (LinearMap.toSpanSingleton R (↑M) x)) ≫
        NatTrans.app φ M)
      1 =
    (forget AddCommGroupCat).map
      (NatTrans.app φ (ModuleCat.of R R) ≫
        (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map
          (ModuleCat.asHomRight (LinearMap.toSpanSingleton R (↑M) x)))
      1
⊢ ↑(NatTrans.app
          ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
            ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ))
          M)
      x =
    ↑(NatTrans.app φ M) x
[PROOFSTEP]
exact w.symm.trans (congr_arg (φ.app M) (one_smul R x))
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x * y) =
      Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x *
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ Equiv.toFun
      { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
        invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
        right_inv :=
          (_ :
            ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
              (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                  ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                φ) }
      (x✝ * y✝) =
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        x✝ *
      Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        y✝
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ (Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x✝ * y✝)).app =
    (Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x✝ *
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y✝).app
[PROOFSTEP]
ext
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ ↑(NatTrans.app
          (Equiv.toFun
            { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
              invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
              right_inv :=
                (_ :
                  ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                    (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                        ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                      φ) }
            (x✝² * y✝))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          (Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              x✝² *
            Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              y✝)
          x✝¹)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ (x✝² * y✝) • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) *
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [AddCommGroupCat.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, mul_smul]
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ x✝² • y✝ • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) *
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x + y) =
      Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x +
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ Equiv.toFun
      { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
        invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
        right_inv :=
          (_ :
            ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
              (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                  ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                φ) }
      (x✝ + y✝) =
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        x✝ +
      Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        y✝
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ (Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x✝ + y✝)).app =
    (Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x✝ +
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y✝).app
[PROOFSTEP]
ext
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ ↑(NatTrans.app
          (Equiv.toFun
            { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
              invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
              right_inv :=
                (_ :
                  ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                    (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                        ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                      φ) }
            (x✝² + y✝))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          (Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              x✝² +
            Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              y✝)
          x✝¹)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ (x✝² + y✝) • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) +
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [AddCommGroupCat.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, add_smul]
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ x✝² • x✝ + y✝ • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) +
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
rfl
