awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x_1 : (↑(M F) : Type (max u v))
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ((((F ⋙
              forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                AddCommGrpCat.carrier)) ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
              (CC := AddCommGrpCat.carrier) AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
              (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
            AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
          AddMonCat.carrier)).ColimitTypeRel
    x y
h₁ :
  (F ⋙
        forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
          (CC := carrier)).ColimitTypeRel
    x y
⊢ Types.FilteredColimit.Rel
    (F ⋙
      forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier))
    x y

Tactic:
apply Types.FilteredColimit.rel_of_colimitTypeRel

Premises used: CategoryTheory.Limits.Types.FilteredColimit.rel_of_colimitTypeRel
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x_1 : (↑(M F) : Type (max u v))
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ((((F ⋙
              forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                AddCommGrpCat.carrier)) ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
              (CC := AddCommGrpCat.carrier) AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
              (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
            AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
          AddMonCat.carrier)).ColimitTypeRel
    x y
⊢ (F ⋙
        forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
          (CC := carrier)).ColimitTypeRel
    x y

Tactic:
h

Premises used: CategoryTheory.Functor.comp
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x_1 : (↑(M F) : Type (max u v))
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ((((F ⋙
              forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                AddCommGrpCat.carrier)) ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
              (CC := AddCommGrpCat.carrier) AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
              (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
            AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
          AddMonCat.carrier)).ColimitTypeRel
    x y
⊢ (F ⋙
        forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
          (CC := carrier)).ColimitTypeRel
    x y

Tactic:
exact h
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
j : J
⊢ Eq (α := (↑(M F) : Type (max u v))) 0 (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 0))

Tactic:
apply AddMonCat.FilteredColimits.colimit_zero_eq

Premises used: AddMonCat.FilteredColimits.colimit_zero_eq
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x y : (j : J) × (↑(F.obj j) : Type (max u v))
k : J
f : x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) ⟶ k
g : y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) ⟶ k
⊢ HAdd.hAdd (α := (↑(M F) : Type (max u v))) (M.mk F x) (M.mk F y) =
    M.mk F
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
        (HAdd.hAdd (α := (↑(F.obj k) : Type (max u v))) (β := (↑(F.obj k) : Type (max u v)))
          ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
                  (F.map f) :
                (a : (↑(F.obj x.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
              (x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
            (↑(F.obj k) : Type (max u v)))
          ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
                  (F.map g) :
                (a : (↑(F.obj y.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
              (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
            (↑(F.obj k) : Type (max u v)))))

Tactic:
apply AddMonCat.FilteredColimits.colimit_add_mk_eq

Premises used: AddMonCat.FilteredColimits.colimit_add_mk_eq
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
j : J
x y : (↑(F.obj j) : Type (max u v))
⊢ HAdd.hAdd (α := (↑(M F) : Type (max u v))) (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x))
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j (x + y))

Tactic:
apply AddMonCat.FilteredColimits.colimit_add_mk_eq'

Premises used: AddMonCat.FilteredColimits.colimit_add_mk_eq'
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x : (j : J) × (↑(F.obj j) : Type (max u v))
⊢ HSMul.hSMul (β := (↑(M F) : Type (max u v))) r (M.mk F x) =
    M.mk F
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
        (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))

Tactic:
rfl

Premises used: ModuleCat.FilteredColimits.M.mk, CategoryTheory.Functor.ιColimitType, rfl, ModuleCat.FilteredColimits.colimitSMulAux
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x : (↑(M F) : Type (max u v))
obtain :
  ∀ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) (r * s)
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) =
      r •
        HSMul.hSMul (β := (↑(M F) : Type (max u v))) s
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x))
⊢ (r * s) • x = r • s • x

Tactic:
obtain ⟨j, x, rfl⟩ := M.mk_surjective F x

Premises used: ModuleCat.FilteredColimits.M.mk_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ HSMul.hSMul (β := (↑(M F) : Type (max u v))) (r * s)
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) =
    r •
      HSMul.hSMul (β := (↑(M F) : Type (max u v))) s
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x))

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x : (↑(M F) : Type (max u v))
obtain :
  ∀ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    HSMul.hSMul (α := R) (β := (↑(M F) : Type (max u v))) 1
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) =
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
⊢ HSMul.hSMul (α := R) 1 x = x

Tactic:
obtain ⟨j, x, rfl⟩ := M.mk_surjective F x

Premises used: ModuleCat.FilteredColimits.M.mk_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ HSMul.hSMul (α := R) (β := (↑(M F) : Type (max u v))) 1
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
rw :
  HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0)) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0)
rw₁ :
  Eq (α := (↑(M F) : Type (max u v)))
    (M.mk F
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))
        (HSMul.hSMul (β :=
          (↑(F.obj
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))) :
            Type (max u v)))
          r
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0) :
            (↑(F.obj
                  (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))) :
              Type (max u v))))))
    (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))
rw₂ rw₃ :
  Eq (α := (↑(M F) : Type (max u v)))
    (M.mk F
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))
        0))
    (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))
⊢ HSMul.hSMul (β := (↑(M F) : Type (max u v))) r 0 = 0

Tactic:
rw [colimit_zero_eq _ (IsFiltered.nonempty.some : J), colimit_smul_mk_eq, smul_zero]

Premises used: ModuleCat.FilteredColimits.colimit_smul_mk_eq, ModuleCat.FilteredColimits.colimit_zero_eq, smul_zero, Nonempty.some, CategoryTheory.IsFiltered.nonempty
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x : (↑(M F) : Type (max u v))
obtain :
  ∀ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    HSMul.hSMul (α := R) (β := (↑(M F) : Type (max u v))) 0
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) =
      0
⊢ HSMul.hSMul (α := R) 0 x = 0

Tactic:
obtain ⟨j, x, rfl⟩ := M.mk_surjective F x

Premises used: ModuleCat.FilteredColimits.M.mk_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ HSMul.hSMul (α := R) (β := (↑(M F) : Type (max u v))) 0
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) =
    0

Tactic:
simp [← colimit_zero_eq]

Premises used: ModuleCat.FilteredColimits.colimit_zero_eq
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (↑(M F) : Type (max u v))
obtain :
  ∀ (i : J) (x : (↑(F.obj i) : Type (max u v))),
    r • (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x) + y) =
      HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
        r • y
⊢ r • (x + y) = r • x + r • y

Tactic:
obtain ⟨i, x, rfl⟩ := M.mk_surjective F x

Premises used: ModuleCat.FilteredColimits.M.mk_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
y : (↑(M F) : Type (max u v))
i : J
x : (↑(F.obj i) : Type (max u v))
obtain :
  ∀ (j : J) (y : (↑(F.obj j) : Type (max u v))),
    r •
        HAdd.hAdd (α := (↑(M F) : Type (max u v)))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) =
      HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
        HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y))
⊢ r • (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x) + y) =
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
      r • y

Tactic:
obtain ⟨j, y, rfl⟩ := M.mk_surjective F y

Premises used: ModuleCat.FilteredColimits.M.mk_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x : (↑(M F) : Type (max u v))
obtain :
  ∀ (i : J) (x : (↑(F.obj i) : Type (max u v))),
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) (r + s)
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) =
      HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
        HSMul.hSMul (β := (↑(M F) : Type (max u v))) s
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x))
⊢ (r + s) • x = r • x + s • x

Tactic:
obtain ⟨i, x, rfl⟩ := M.mk_surjective F x

Premises used: ModuleCat.FilteredColimits.M.mk_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
i : J
x : (↑(F.obj i) : Type (max u v))
⊢ HSMul.hSMul (β := (↑(M F) : Type (max u v))) (r + s)
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) =
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
      HSMul.hSMul (β := (↑(M F) : Type (max u v))) s
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x))

Tactic:
simp [_root_.add_smul, colimit_add_mk_eq']

Premises used: ModuleCat.FilteredColimits.colimit_add_mk_eq', add_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
j : J
⊢ ∀ (m : R) (x : (↑(F.1 j) : Type (max u v))),
    (↑(AddCommGrpCat.Hom.hom
                ((AddCommGrpCat.FilteredColimits.colimitCocone.{v, u}
                        (F ⋙
                          forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                            (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                            fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                            AddCommGrpCat.carrier))).ι.app
                  j)) :
            ZeroHom (↑((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat).obj j) : Type (max v u))
              (↑(((Functor.const J).obj
                        (AddCommGrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)).pt).obj
                    j) :
                Type (max v u))).toFun
        (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ((↑(AddCommGrpCat.Hom.hom
                  ((AddCommGrpCat.FilteredColimits.colimitCocone.{v, u}
                          (F ⋙
                            forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                              (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                              fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                              AddCommGrpCat.carrier))).ι.app
                    j)) :
              ZeroHom (↑((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat).obj j) : Type (max v u))
                (↑(((Functor.const J).obj
                          (AddCommGrpCat.FilteredColimits.colimitCocone
                              (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)).pt).obj
                      j) :
                  Type (max v u))).toFun
          x)

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x x_1 : J
f : x ⟶ x_1
hf :
  ∀ (x_2 : (↑(F.obj x) : Type (max u v))),
    Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
      ((Hom.hom (F.map f ≫ coconeMorphism F x_1) :
            (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
          x_2 :
        (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
      ((Hom.hom
              (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const J) (colimit F)) x) (coconeMorphism F x)
                (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit F)) f)) :
            (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
          x_2 :
        (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
⊢ Eq (α := F.obj x ⟶ Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) (F.map f ≫ coconeMorphism F x_1)
    (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const J) (colimit F)) x) (coconeMorphism F x)
      (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit F)) f))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x x_1 : J
f : x ⟶ x_1
x_2 : (↑(F.obj x) : Type (max u v))
⊢ Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
    ((Hom.hom (F.map f ≫ coconeMorphism F x_1) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
    ((Hom.hom
            (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const J) (colimit F)) x) (coconeMorphism F x)
              (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit F)) f)) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))

Tactic:
simpa using (Types.TypeMax.colimitCocone
          (F ⋙ forget (ModuleCat R))).ι.naturality_apply f _

Premises used: CategoryTheory.NatTrans.naturality_apply, ModuleCat, CategoryTheory.Limits.Types.TypeMax.colimitCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.Cocone.ι, CategoryTheory.forget