awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
X Y : ModuleCat.{u_1, u} R
i : X ≅ Y
⊢ Hom.hom i.hom ∘ₗ Hom.hom i.inv = LinearMap.id

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
X Y : ModuleCat.{u_1, u} R
i : X ≅ Y
⊢ Hom.hom i.inv ∘ₗ Hom.hom i.hom = LinearMap.id

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{u_1, u} R
i : X ≅ Y
x : (↑X : Type u_1)
⊢ Eq (α := (↑Y : Type u_1)) ((i.toLinearEquiv : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC :=
            carrier) i.hom :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1))
        x :
      (↑Y : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{u_1, u} R
i : X ≅ Y
⊢ i.toLinearEquiv.symm = i.symm.toLinearEquiv

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.ofLinear, CategoryTheory.Iso.toLinearEquiv, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{u_1, u} R
i : X ≅ Y
⊢ (↑i.toLinearEquiv : (↑X : Type u_1) →ₗ[R] (↑Y : Type u_1)) = Hom.hom i.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f g : M ⟶ N
⊢ Hom.hom (f + g) = Hom.hom f + Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ Eq.{v + 1} (α := (↑M : Type v) →ₗ[R] (↑N : Type v)) (Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
n : ℕ
f : M ⟶ N
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ Hom.hom (-f) = -Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f g : M ⟶ N
⊢ Hom.hom (f - g) = Hom.hom f - Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
n : ℤ
f : M ⟶ N
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
ι : Type u_1
f : ι → (M ⟶ N)
s : Finset ι
⊢ Eq.{v + 1} (α := (↑M : Type v) →ₗ[R] (↑N : Type v)) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))

Tactic:
map_sum ({ toFun := ModuleCat.Hom.hom, map_zero' := ModuleCat.hom_zero, map_add' := hom_add } :
    (M ⟶ N) →+ (M →ₗ[R] N)) _ _

Premises used: ModuleCat.hom_zero, AddMonoidHom.mk, map_sum, ZeroHom.mk, ModuleCat.hom_add, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
h : IsZero M
⊢ Subsingleton.{v + 1} (↑M : Type v)

Tactic:
subsingleton_of_forall_eq 0 (fun x ↦ ?_)

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
h : IsZero M
refine : ∀ (x : (↑M : Type v)), x = 0
⊢ Subsingleton.{v + 1} (↑M : Type v)

Tactic:
refine subsingleton_of_forall_eq 0 (fun x ↦ ?_)

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
h : IsZero M
x : (↑M : Type v)
rw :
  Eq (α := (↑M : Type v)) ((Hom.hom (𝟙 M) : (a : (↑M : Type v)) → (↑M : Type v)) x : (↑M : Type v)) (0 : (↑M : Type v))
⊢ x = 0

Tactic:
rw [← LinearMap.id_apply (R := R) x, ← ModuleCat.hom_id]

Premises used: LinearMap.id_apply, ModuleCat.hom_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
h : IsZero M
x : (↑M : Type v)
⊢ Eq (α := (↑M : Type v)) ((Hom.hom (𝟙 M) : (a : (↑M : Type v)) → (↑M : Type v)) x : (↑M : Type v)) (0 : (↑M : Type v))

Tactic:
simp only [(CategoryTheory.Limits.IsZero.iff_id_eq_zero M).mp h, hom_zero, LinearMap.zero_apply]

Premises used: ModuleCat.hom_zero, LinearMap.zero_apply, Iff.mp, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsZero (C := ModuleCat.{u_1, u} R) (of R M) ↔ Subsingleton M

Tactic:
isZero_iff_subsingleton

Premises used: ModuleCat.isZero_iff_subsingleton
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
⊢ Eq.{v + 1} (α := Quiver.Hom (V := ModuleCat.{v, u} R) (of R M) (of R N)) (↟0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f g : M →ₗ[R] N
⊢ ↟(f + g) = ↟f + ↟g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
S : Type u_1
inst_1 : Monoid S
inst_2 : DistribMulAction.{u_1, v} S (↑N : Type v)
inst_3 : SMulCommClass.{u, u_1, v} R S (↑N : Type v)
s : S
f : M ⟶ N
⊢ Hom.hom (s • f) = s • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
x : S₀
x_1 : S
x_2 : (↑M : Type v)
rw : HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) x : S) (x_1 • x_2) = x • x_1 • x_2
⊢ (x • x_1) • x_2 = x • x_1 • x_2

Tactic:
rw [Algebra.smul_def, mul_smul]

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
x : S₀
x_1 : S
x_2 : (↑M : Type v)
⊢ HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) x : S) (x_1 • x_2) = x • x_1 • x_2

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₁ :
  HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₂ :
  HMul.hMul (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) s • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₃ rw₄ :
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n) =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)

Tactic:
rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]

Premises used: smul_assoc, smul_eq_mul, SemigroupAction.mul_smul, Algebra.commutes
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M_1 N_1 x M N : ModuleCat.{v, u} S
s₀ : S₀
f : x ⟶ M
g : M ⟶ N
hf :
  ∀ (x_1 : (↑x : Type v)),
    Eq (α := (↑N : Type v)) ((Hom.hom ((s₀ • f) ≫ g) : (a : (↑x : Type v)) → (↑N : Type v)) x_1 : (↑N : Type v))
      ((Hom.hom (s₀ • f ≫ g) : (a : (↑x : Type v)) → (↑N : Type v)) x_1 : (↑N : Type v))
⊢ (s₀ • f) ≫ g = s₀ • f ≫ g

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M_1 N_1 x M N : ModuleCat.{v, u} S
s₀ : S₀
f : x ⟶ M
g : M ⟶ N
x_1 : (↑x : Type v)
⊢ Eq (α := (↑N : Type v)) ((Hom.hom ((s₀ • f) ≫ g) : (a : (↑x : Type v)) → (↑N : Type v)) x_1 : (↑N : Type v))
    ((Hom.hom (s₀ • f ≫ g) : (a : (↑x : Type v)) → (↑N : Type v)) x_1 : (↑N : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
S : Type u
inst : CommRing S
M : ModuleCat.{v, u} S
s : S
⊢ ↟((LinearMap.lsmul S (↑M : Type v) : (a : S) → (↑M : Type v) →ₗ[S] (↑M : Type v)) s) =
    HSMul.hSMul (β := M ⟶ M) s (𝟙 M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
S : Type u
inst : CommRing S
X Y X' Y' : ModuleCat.{v, u} S
i : X ≅ X'
j : Y ≅ Y'
f : X ⟶ Y
⊢ Eq (α := X' ⟶ Y') ((i.homCongr j : (a : X ⟶ Y) → X' ⟶ Y') f : X' ⟶ Y')
    ({
        hom' :=
          ((i.toLinearEquiv.arrowCongr (R₁' := S) (R₂' := S) (M₁' := (↑Y : Type v)) (M₂' := (↑Y' : Type v)) (σ₁'₂' :=
                  RingHom.id S) (σ₂'₁' := RingHom.id S) (σ₁₁' := RingHom.id S) (σ₂₂' := RingHom.id S) (σ₂₁' :=
                  RingHom.id S) (σ₁₂' := RingHom.id S) j.toLinearEquiv :
                ((↑X : Type v) →ₗ[S] (↑Y : Type v)) ≃ₗ[S] (↑X' : Type v) →ₗ[S] (↑Y' : Type v)) :
              (a : (↑X : Type v) →ₗ[S] (↑Y : Type v)) → (↑X' : Type v) →ₗ[S] (↑Y' : Type v))
            (Hom.hom f) } :
      X'.Hom Y')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
S : Type u
inst : CommRing S
X X' : ModuleCat.{v, u} S
i : X ≅ X'
f : End X
⊢ Eq (α := End X') ((i.conj : (a : End X) → End X') f : End X')
    ({
        hom' :=
          ((LinearEquiv.conj.{u, u, v, v} (R₁' := S) (R₂' := S) (M₁' := (↑X : Type v)) (M₂' := (↑X' : Type v)) (σ₁'₂' :=
                  RingHom.id S) (σ₂'₁' := RingHom.id S) i.toLinearEquiv :
                Module.End S (↑X : Type v) ≃ₗ[S] Module.End S (↑X' : Type v)) :
              (a : Module.End S (↑X : Type v)) → Module.End S (↑X' : Type v))
            (Hom.hom f) } :
      X'.Hom X')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
r : R
rw rw₁ : Eq.{v + 1} (α := (↑M : Type v)) 0 0
⊢ HSMul.hSMul (β := (↑M : Type v)) r 0 = 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
r : R
x y : (↑M : Type v)
rw rw₁ : r • x + r • y = r • x + r • y
⊢ r • (x + y) = r • x + r • y

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
x : (↑(AddCommGrpCat.of (↑M : Type v)) : Type v)
⊢ Eq (α := (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier)
            (AddCommGrpCat.ofHom
              { toFun := fun (m : (↑M : Type v)) ↦ HSMul.hSMul.{u, v, v} (α := R) 1 m, map_zero' := ⋯, map_add' := ⋯ :
                (↑M : Type v) →+ (↑M : Type v) }) :
          (a : (↑(AddCommGrpCat.of (↑M : Type v)) : Type v)) → (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
        x :
      (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
            (AddCommGrpCat.of (↑M : Type v)) (AddCommGrpCat.of (↑M : Type v)) 1 :
          (a : (↑(AddCommGrpCat.of (↑M : Type v)) : Type v)) → (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
        x :
      (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
x : (↑(AddCommGrpCat.of (↑M : Type v)) : Type v)
⊢ Eq (α := (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier)
            (AddCommGrpCat.ofHom
              { toFun := fun (m : (↑M : Type v)) ↦ HSMul.hSMul.{u, v, v} (α := R) 0 m, map_zero' := ⋯, map_add' := ⋯ :
                (↑M : Type v) →+ (↑M : Type v) }) :
          (a : (↑(AddCommGrpCat.of (↑M : Type v)) : Type v)) → (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
        x :
      (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
            (AddCommGrpCat.of (↑M : Type v)) (AddCommGrpCat.of (↑M : Type v)) 0 :
          (a : (↑(AddCommGrpCat.of (↑M : Type v)) : Type v)) → (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))
        x :
      (↑(AddCommGrpCat.of (↑M : Type v)) : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
r : R
x :
  (↑(Functor.obj
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        M) :
    Type v)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
            (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
            (CD := AddCommGrpCat.carrier))
          N) :
      Type v))
    ((AddCommGrpCat.Hom.hom
            (CategoryTheory.Functor.map
                (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦
                  (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD :=
                  fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                f ≫
              (N.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj N)) r) :
          (a : (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj M) : Type v)) →
            (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj N) : Type v))
        x :
      (↑(Functor.obj
            (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
              (CD := AddCommGrpCat.carrier))
            N) :
        Type v))
    ((AddCommGrpCat.Hom.hom
            ((M.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj M)) r ≫
              CategoryTheory.Functor.map
                (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦
                  (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD :=
                  fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                f) :
          (a : (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj M) : Type v)) →
            (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj N) : Type v))
        x :
      (↑(Functor.obj
            (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
              (CD := AddCommGrpCat.carrier))
            N) :
        Type v))

Tactic:
(f.hom.map_smul r x).symm

Premises used: LinearMap.map_smul, Eq.symm, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
r : R
x :
  (↑(Functor.obj
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        M) :
    Type v)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
            (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
            (CD := AddCommGrpCat.carrier))
          N) :
      Type v))
    ((AddCommGrpCat.Hom.hom
            (CategoryTheory.Functor.map
                (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦
                  (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD :=
                  fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                f ≫
              (N.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj N)) r) :
          (a : (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj M) : Type v)) →
            (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj N) : Type v))
        x :
      (↑(Functor.obj
            (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
              (CD := AddCommGrpCat.carrier))
            N) :
        Type v))
    ((AddCommGrpCat.Hom.hom
            ((M.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj M)) r ≫
              CategoryTheory.Functor.map
                (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦
                  (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD :=
                  fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                f) :
          (a : (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj M) : Type v)) →
            (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj N) : Type v))
        x :
      (↑(Functor.obj
            (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
              (CD := AddCommGrpCat.carrier))
            N) :
        Type v))

Tactic:
exact (f.hom.map_smul r x).symm

Premises used: LinearMap.map_smul, Eq.symm, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
r : R
x : (↑(mkOfSMul' φ) : Type u_1)
⊢ r • x =
    (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
          (fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) AddCommGrpCat.carrier _ _ A A
          (have this : A ⟶ A := (φ : (a : R) → End A) r;
          this) :
        (a : (↑A : Type u_1)) → (↑A : Type u_1))
      x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
⊢ ∀ (x y : R) (b : (↑(mkOfSMul' φ) : Type u_1)), (x * y) • b = x • y • b

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
⊢ ∀ (b : (↑(mkOfSMul' φ) : Type u_1)), HSMul.hSMul.{u, u_1, u_1} (α := R) 1 b = b

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
x x_1 : R
x_2 : (↑(mkOfSMul' φ) : Type u_1)
simp :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
          AddCommGrpCat.carrier)
          (HAdd.hAdd (α := End A) (β := End A) ((φ : (a : R) → End A) x : End A) ((φ : (a : R) → End A) x_1 : End A)) :
        (a : (↑A : Type u_1)) → (↑A : Type u_1))
      x_2 =
    HAdd.hAdd (α := (↑(mkOfSMul' φ) : Type u_1)) (β := (↑(mkOfSMul' φ) : Type u_1))
      ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
              (fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) AddCommGrpCat.carrier _ _ A A
              ((φ : (a : R) → End A) x) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          x_2 :
        (↑A : Type u_1))
      ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
              (fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) AddCommGrpCat.carrier _ _ A A
              ((φ : (a : R) → End A) x_1) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          x_2 :
        (↑A : Type u_1))
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
x x_1 : R
x_2 : (↑(mkOfSMul' φ) : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
          AddCommGrpCat.carrier)
          (HAdd.hAdd (α := End A) (β := End A) ((φ : (a : R) → End A) x : End A) ((φ : (a : R) → End A) x_1 : End A)) :
        (a : (↑A : Type u_1)) → (↑A : Type u_1))
      x_2 =
    HAdd.hAdd (α := (↑(mkOfSMul' φ) : Type u_1)) (β := (↑(mkOfSMul' φ) : Type u_1))
      ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
              (fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) AddCommGrpCat.carrier _ _ A A
              ((φ : (a : R) → End A) x) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          x_2 :
        (↑A : Type u_1))
      ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
              (fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) AddCommGrpCat.carrier _ _ A A
              ((φ : (a : R) → End A) x_1) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          x_2 :
        (↑A : Type u_1))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
⊢ ∀ (x : (↑(mkOfSMul' φ) : Type u_1)), HSMul.hSMul.{u, u_1, u_1} (α := R) 0 x = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
r : R
⊢ Eq.{u_1 + 1} (α :=
    End
      (Functor.obj
        (forget₂ (ModuleCat.{u_1, u} R) (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
          (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) AddCommGrpCat (FD :=
          fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD := AddCommGrpCat.carrier))
        (mkOfSMul φ)))
    (((mkOfSMul φ).smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj (mkOfSMul φ))) r :
      End
        (Functor.obj
          (forget₂ (ModuleCat.{u_1, u} R) (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
            (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD := AddCommGrpCat.carrier))
          (mkOfSMul φ)))
    ((φ : (a : R) → End A) r : End A)

Tactic:
rfl

Premises used: CategoryTheory.End, rfl