[GOAL]
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
⊢ AddHom.toFun
      { toFun := ↑f,
        map_add' :=
          (_ :
            ∀ (a b : ↑A),
              ↑(let_fun this := f;
                    this)
                  (a + b) =
                ↑(let_fun this := f;
                      this)
                    a +
                  ↑(let_fun this := f;
                      this)
                    b) }
      (n • x) =
    ↑(RingHom.id ℤ) n •
      AddHom.toFun
        { toFun := ↑f,
          map_add' :=
            (_ :
              ∀ (a b : ↑A),
                ↑(let_fun this := f;
                      this)
                    (a + b) =
                  ↑(let_fun this := f;
                        this)
                      a +
                    ↑(let_fun this := f;
                        this)
                      b) }
        x
[PROOFSTEP]
convert AddMonoidHom.map_zsmul (show A.carrier →+ B.carrier from f) x n
[GOAL]
case h.e'_2.h.e'_1.h.e'_4.h.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
⊢ SMulZeroClass.toSMul = SubNegMonoid.SMulInt
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_4.h.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
⊢ SMulZeroClass.toSMul = SubNegMonoid.SMulInt
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.e'_1.h.e'_4.h.e'_3.smul.h.h
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
x✝¹ : ℤ
x✝ : ↑A
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
[PROOFSTEP]
apply int_smul_eq_zsmul
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.smul.h.h
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
x✝¹ : (fun x => ℤ) n
x✝ : ↑B
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
[PROOFSTEP]
apply int_smul_eq_zsmul
