awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x : (↑G : Type u)
mem : x ∈ (Hom.hom f).ker
⊢ Eq.{u + 1} (α := (↑G : Type u))
    (↑((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (Y := of ↥(Hom.hom f).ker)
              (CategoryStruct.comp (Y := kernel f) (kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯)
                (ofHom
                  {
                    toFun := fun (g : (↑(limit.cone (parallelPair f 0)).1 : Type u)) ↦
                      Subtype.mk (p := fun (x : (↑G : Type u)) ↦ x ∈ (Hom.hom f).ker)
                        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                              (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier) (X := kernel f) (kernel.ι f) :
                            (a : (↑(kernel f) : Type u)) → (↑G : Type u))
                          g)
                        ⋯,
                    map_zero' := ⋯, map_add' := ⋯ })) :
            (a : (↑(of ↥(Hom.hom f).ker) : Type u)) → (↑(of ↥(Hom.hom f).ker) : Type u))
          (Subtype.mk (p := fun (x : (↑G : Type u)) ↦ x ∈ (Hom.hom f).ker) x mem)) :
      (↑G : Type u))
    (↑((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (𝟙 (of ↥(Hom.hom f).ker)) :
            (a : (↑(of ↥(Hom.hom f).ker) : Type u)) → (↑(of ↥(Hom.hom f).ker) : Type u))
          (Subtype.mk (p := fun (x : (↑G : Type u)) ↦ x ∈ (Hom.hom f).ker) x mem)) :
      (↑G : Type u))

Tactic:
apply ConcreteCategory.congr_hom (kernel.lift_ι f _ _)

Premises used: CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
hf :
  ∀ (x : (↑(kernel f) : Type u)),
    Eq (α := (↑(of (↑G : Type u)) : Type u))
      ((Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype) :
            (a : (↑(kernel f) : Type u)) → (↑(of (↑G : Type u)) : Type u))
          x :
        (↑(of (↑G : Type u)) : Type u))
      ((Hom.hom (kernel.ι f) : (a : (↑(kernel f) : Type u)) → (↑(of (↑G : Type u)) : Type u)) x :
        (↑(of (↑G : Type u)) : Type u))
⊢ (kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype = kernel.ι f

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : (↑(kernel f) : Type u)
⊢ Eq (α := (↑(of (↑G : Type u)) : Type u))
    ((Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype) :
          (a : (↑(kernel f) : Type u)) → (↑(of (↑G : Type u)) : Type u))
        x :
      (↑(of (↑G : Type u)) : Type u))
    ((Hom.hom (kernel.ι f) : (a : (↑(kernel f) : Type u)) → (↑(of (↑G : Type u)) : Type u)) x :
      (↑(of (↑G : Type u)) : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
⊢ (kernelIsoKer f).inv ≫ kernel.ι f = ofHom (Hom.hom f).ker.subtype

Tactic:
simp [kernelIsoKer]

Premises used: AddCommGrpCat.kernelIsoKer
-- Module: Mathlib.Algebra.Category.Grp.Preadditive
Goal:
M N : AddCommGrpCat
f g : M ⟶ N
⊢ Hom.hom (f + g) = Hom.hom f + Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Preadditive
Goal:
P Q : AddCommGrpCat
f g : P ⟶ Q
x : (↑P : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC := carrier)
          (f + g) :
        (a : (↑P : Type u_1)) → (↑Q : Type u_1))
      x =
    HAdd.hAdd (α := (↑Q : Type u_1)) (β := (↑Q : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
              carrier) f :
            (a : (↑P : Type u_1)) → (↑Q : Type u_1))
          x :
        (↑Q : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
              carrier) g :
            (a : (↑P : Type u_1)) → (↑Q : Type u_1))
          x :
        (↑Q : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Preadditive
Goal:
M N : AddCommGrpCat
⊢ Eq.{u + 1} (α := (↑M : Type u) →+ (↑N : Type u)) (Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Preadditive
Goal:
M N : AddCommGrpCat
n : ℕ
f : M ⟶ N
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Preadditive
Goal:
M N : AddCommGrpCat
f : M ⟶ N
⊢ Hom.hom (-f) = -Hom.hom f

Tactic:
rfl

Premises used: AddMonoidHom.mk', rfl
-- Module: Mathlib.Algebra.Category.Grp.Preadditive
Goal:
M N : AddCommGrpCat
f g : M ⟶ N
⊢ Hom.hom (f - g) = Hom.hom f - Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Preadditive
Goal:
M N : AddCommGrpCat
n : ℤ
f : M ⟶ N
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F : CategoryTheory.Functor.{v, w', u, w' + 1} C GrpCat
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
⊢ FunctorToTypes.Small.{w, w', v, u}
    (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{w'}) ↦ (↑x1 : Type w') →* (↑x2 : Type w')) (CC := GrpCat.carrier))

Tactic:
fun X ↦ inferInstanceAs <| Small.{w} (F.obj X)

Premises used: _private.0.instSmallCompGrpCatForgetMonoidHomCarrierOfSmallObj._proof_1
-- Module: Mathlib.Algebra.Category.Grp.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w', u, w' + 1} C GrpCat
τ : F ⟶ G
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
inst_2 : ∀ (X : C), Small.{w, w'} (↑(G.obj X) : Type w')
X Y : C
f : X ⟶ Y
hf :
  ∀ (x : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)),
    Eq (α := (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
      ((Hom.hom
              ((shrinkFunctor.{w, w', v, u} F).map f ≫
                ofHom
                  (MonoidHom.comp
                    (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
                    (MulEquiv.toMonoidHom Shrink.mulEquiv))) :
            (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
              (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
          x :
        (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
      ((Hom.hom
              (ofHom
                  (MonoidHom.comp
                    (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
                    (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
                (shrinkFunctor.{w, w', v, u} G).map f) :
            (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
              (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
          x :
        (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
⊢ (shrinkFunctor.{w, w', v, u} F).map f ≫
      ofHom
        (MonoidHom.comp (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
          (MulEquiv.toMonoidHom Shrink.mulEquiv)) =
    ofHom
        (MonoidHom.comp (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
          (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
      (shrinkFunctor.{w, w', v, u} G).map f

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w', u, w' + 1} C GrpCat
τ : F ⟶ G
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
inst_2 : ∀ (X : C), Small.{w, w'} (↑(G.obj X) : Type w')
X Y : C
f : X ⟶ Y
x : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)
⊢ Eq (α := (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            ((shrinkFunctor.{w, w', v, u} F).map f ≫
              ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv))) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            (ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
              (shrinkFunctor.{w, w', v, u} G).map f) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))

Tactic:
congr($((FunctorToTypes.shrinkMap.{w} (Functor.whiskerRight τ (forget _))).naturality f) x)

Premises used: GrpCat, congrArg, CategoryTheory.ConcreteCategory.hom, id, CategoryTheory.Functor.whiskerRight, CategoryTheory.NatTrans.naturality, CategoryTheory.forget, DFunLike.coe, CategoryTheory.FunctorToTypes.shrinkMap
-- Module: Mathlib.Algebra.Category.Grp.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w', u, w' + 1} C GrpCat
τ : F ⟶ G
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
inst_2 : ∀ (X : C), Small.{w, w'} (↑(G.obj X) : Type w')
X Y : C
f : X ⟶ Y
x : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)
⊢ Eq (α := (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            ((shrinkFunctor.{w, w', v, u} F).map f ≫
              ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv))) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            (ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
              (shrinkFunctor.{w, w', v, u} G).map f) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))

Tactic:
exact
      congr($((FunctorToTypes.shrinkMap.{w} (Functor.whiskerRight τ (forget _))).naturality f) x)
-- Module: Mathlib.Algebra.Category.Grp.Subobject
Goal:
⊢ WellPowered.{u, u, u + 1} AddCommGrpCat

Tactic:
wellPowered_of_equiv.{u} (forget₂ (ModuleCat.{u} ℤ) AddCommGrpCat.{u}).asEquivalence

Premises used: ModuleCat, Int, CategoryTheory.Functor.asEquivalence, CategoryTheory.forget₂, CategoryTheory.wellPowered_of_equiv, AddCommGrpCat
-- Module: Mathlib.Algebra.Category.Grp.Ulift
Goal:
⊢ uliftFunctor.Faithful

Tactic:
uliftFunctorFullyFaithful.faithful

Premises used: GrpCat.uliftFunctorFullyFaithful, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.Algebra.Category.Grp.Ulift
Goal:
⊢ uliftFunctor.Full

Tactic:
uliftFunctorFullyFaithful.full

Premises used: GrpCat.uliftFunctorFullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.Grp.Ulift
Goal:
⊢ uliftFunctor.Faithful

Tactic:
uliftFunctorFullyFaithful.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CommGrpCat.uliftFunctorFullyFaithful
-- Module: Mathlib.Algebra.Category.Grp.Ulift
Goal:
⊢ uliftFunctor.Full

Tactic:
uliftFunctorFullyFaithful.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CommGrpCat.uliftFunctorFullyFaithful
-- Module: Mathlib.Algebra.Category.Grp.Ulift
Goal:
J : Type w
x : Category.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u + 1} J AddCommGrpCat
c : Cocone F
hc : IsColimit c
rw :
  Function.Bijective (α := Colimits.Quot F) (β := (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))
    (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) (Quot.desc F c)) :
      (a : Colimits.Quot F) → (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))

Tactic:
rw [isColimit_iff_bijective_desc, ← Function.Bijective.of_comp_iff _
          (quotQuotUliftAddEquiv F).bijective, ← AddEquiv.coe_toAddMonoidHom,
          ← AddMonoidHom.coe_comp, Quot.desc_quotQuotUliftAddEquiv]

Premises used: AddCommGrpCat.isColimit_iff_bijective_desc, AddCommGrpCat.Colimits.quotQuotUliftAddEquiv, AddEquiv.bijective, Function.Bijective.of_comp_iff, AddMonoidHom.coe_comp, AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv, AddEquiv.coe_toAddMonoidHom
-- Module: Mathlib.Algebra.Category.Grp.Ulift
Goal:
J : Type w
x : Category.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u + 1} J AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Function.Bijective (α := Colimits.Quot F) (β := (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))
    (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) (Quot.desc F c)) :
      (a : Colimits.Quot F) → (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))

Tactic:
ULift.up_bijective.comp ((isColimit_iff_bijective_desc c).mp (Nonempty.intro hc))

Premises used: ULift.up_bijective, AddCommGrpCat.isColimit_iff_bijective_desc, Nonempty.intro, Iff.mp, Function.Bijective.comp
-- Module: Mathlib.Algebra.Category.Grp.Ulift
Goal:
J : Type w
x : Category.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u + 1} J AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Function.Bijective (α := Colimits.Quot F) (β := (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))
    (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) (Quot.desc F c)) :
      (a : Colimits.Quot F) → (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))

Tactic:
exact ULift.up_bijective.comp ((isColimit_iff_bijective_desc c).mp (Nonempty.intro hc))

Premises used: ULift.up_bijective, AddCommGrpCat.isColimit_iff_bijective_desc, Nonempty.intro, Iff.mp, Function.Bijective.comp
-- Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
⊢ (AddCommGrpCat.Hom.hom f :
        (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
          (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u))
      (n • x) =
    HSMul.hSMul (β :=
      (↑(Functor.obj
            (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
              carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            B) :
        Type u))
      n
      ((AddCommGrpCat.Hom.hom f :
            (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
              (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u))
          x :
        (↑(Functor.obj
              (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
                carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              B) :
          Type u))

Tactic:
AddMonoidHom.map_zsmul f.hom n x

Premises used: AddMonoidHom.map_zsmul, AddCommGrpCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
h :
  (↑B : Type u) =
      (↑(Functor.obj
            (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
              carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            B) :
        Type u) →
    (↑A : Type u) =
        (↑(Functor.obj
              (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
                carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              A) :
          Type u) →
      Eq.{u + 1} (α := SMul ℤ (↑A : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul
h₁ :
  (↑B : Type u) =
      (↑(Functor.obj
            (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
              carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            B) :
        Type u) →
    Eq.{u + 1} (α := SMul ℤ (↑B : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul
⊢ AddHom.toFun
      {
        toFun :=
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) f) :
            (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
              (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u)),
        map_add' := ⋯ : (↑A : Type u) →ₙ+ (↑B : Type u) }
      (n • x) =
    HSMul.hSMul (α := ℤ) ((RingHom.id ℤ : (a : ℤ) → ℤ) n : ℤ)
      (AddHom.toFun
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) f) :
              (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
                (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u)),
          map_add' := ⋯ : (↑A : Type u) →ₙ+ (↑B : Type u) }
        x)

Tactic:
convert! AddMonoidHom.map_zsmul f.hom n x

Premises used: AddMonoidHom.map_zsmul, AddCommGrpCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
e_1 :
  (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u)
e_2 :
  (↑A : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          A) :
      Type u)
h : ∀ (x : ℤ) (x_1 : (↑A : Type u)), SMul.smul x x_1 = SMul.smul x x_1
⊢ Eq.{u + 1} (α := SMul ℤ (↑A : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
e_1 :
  (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u)
h : ∀ (x : ℤ) (x_1 : (↑B : Type u)), SMul.smul x x_1 = SMul.smul x x_1
⊢ Eq.{u + 1} (α := SMul ℤ (↑B : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
e_1 :
  (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u)
e_2 :
  (↑A : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          A) :
      Type u)
x_1 : ℤ
x_2 : (↑A : Type u)
⊢ SMul.smul x_1 x_2 = SMul.smul x_1 x_2

Tactic:
apply int_smul_eq_zsmul

Premises used: int_smul_eq_zsmul
-- Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
e_1 :
  (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u)
x_1 : ℤ
x_2 : (↑B : Type u)
⊢ SMul.smul x_1 x_2 = SMul.smul x_1 x_2

Tactic:
apply int_smul_eq_zsmul

Premises used: int_smul_eq_zsmul