-- Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
theorem colimitModule.one_smul (x : (M F)) : (1 : R) • x = x

Proof state:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x : ↑(M F)
⊢ 1 • x = 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
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          a =
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        a

Proof state:
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat 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, 1 • ⟨j, x⟩.snd⟩ =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
          forget AddMonCat))
      ⟨j, x⟩

Tactic:
simp

Result:
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F ⟨j, x⟩ =
    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
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F ⟨j, x⟩ =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
          forget AddMonCat))
      ⟨j, x⟩

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          a =
      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
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        x =
    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
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          a =
      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
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
              forget AddMonCat))
          a =
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        a

Proof state:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        x =
    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
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        ⟨j, x⟩ =
    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
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
            forget AddMonCat))
        ⟨j, x⟩ =
    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 F 1 ⟨j, x⟩]

Result:
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat 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, 1 • ⟨j, x⟩.snd⟩ =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙
          forget AddMonCat))
      ⟨j, x⟩