-- 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:
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)⟩

Tactic:
rfl

Result:
no goals

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
⊢ (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⟩

Tactic:
erw [colimit_smul_mk_eq, _root_.add_smul, colimit_smul_mk_eq, colimit_smul_mk_eq,
    colimit_add_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]

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, 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⟩

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)
⊢ (r + s) • x = r • x + s • x

Tactic:
refine Quot.inductionOn 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 : ↑(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