-- Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
theorem colimitModule.add_smul (r s : R) (x : (M F)) : (r + s) • x = r • x + s • x

Proof state:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    (r + s) •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          a =
      r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
                forget AddMonCat))
            a +
        s •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
                forget AddMonCat))
            a

Tactic:
intro x

Result:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ (r + s) •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        x =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          x +
      s •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          x

Proof state:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ (r + s) •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        x =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          x +
      s •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          x

Tactic:
obtain ⟨j, x⟩ := x

Result:
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ (r + s) •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        ⟨j, x⟩ =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          ⟨j, x⟩ +
      s •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          ⟨j, x⟩

Proof state:
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F ⟨⟨j, x⟩.fst, r • ⟨j, x⟩.snd + s • ⟨j, x⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk
      (((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat)
      ⟨j,
        (ConcreteCategory.hom
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat).map
                (𝟙 j)))
            ⟨j, r • ⟨j, x⟩.snd⟩.snd +
          (ConcreteCategory.hom
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat).map
                (𝟙 j)))
            ⟨j, s • ⟨j, x⟩.snd⟩.snd⟩

Tactic:
simp only [Functor.comp_obj, forget₂_obj, Functor.comp_map, CategoryTheory.Functor.map_id,
  forget₂_map]

Result:
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F ⟨j, r • x + s • x⟩ =
    AddMonCat.FilteredColimits.M.mk
      (((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat)
      ⟨j,
        (ConcreteCategory.hom
              ((forget₂ AddGrp AddMonCat).map
                ((forget₂ AddCommGrp AddGrp).map (AddCommGrp.ofHom ↑(Hom.hom (𝟙 (F.obj j)))))))
            (r • x) +
          (ConcreteCategory.hom
              ((forget₂ AddGrp AddMonCat).map
                ((forget₂ AddCommGrp AddGrp).map (AddCommGrp.ofHom ↑(Hom.hom (𝟙 (F.obj j)))))))
            (s • x)⟩

Proof state:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    (r + s) •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          a =
      r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
                forget AddMonCat))
            a +
        s •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
                forget AddMonCat))
            a

Tactic:
clear x

Result:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    (r + s) •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          a =
      r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
                forget AddMonCat))
            a +
        s •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
                forget AddMonCat))
            a