[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ colimitSMulAux F r x = colimitSMulAux F r y
[PROOFSTEP]
apply M.mk_eq
[GOAL]
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ ∃ k f g, ↑(F.map f) { fst := x.fst, snd := r • x.snd }.snd = ↑(F.map g) { fst := y.fst, snd := r • y.snd }.snd
[PROOFSTEP]
obtain ⟨k, f, g, hfg⟩ := h
[GOAL]
case h.intro.intro.intro
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd
⊢ ∃ k f g, ↑(F.map f) { fst := x.fst, snd := r • x.snd }.snd = ↑(F.map g) { fst := y.fst, snd := r • y.snd }.snd
[PROOFSTEP]
use k, f, g
[GOAL]
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd
⊢ ↑(F.map f) { fst := x.fst, snd := r • x.snd }.snd = ↑(F.map g) { fst := y.fst, snd := r • y.snd }.snd
[PROOFSTEP]
simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg 
[GOAL]
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : ↑(F.map f) x.snd = ↑(F.map g) y.snd
⊢ ↑(F.map f) { fst := x.fst, snd := r • x.snd }.snd = ↑(F.map g) { fst := y.fst, snd := r • y.snd }.snd
[PROOFSTEP]
simp [hfg]
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x : ↑(M F)
⊢ ↑(M F)
[PROOFSTEP]
refine' Quot.lift (colimitSMulAux F r) _ x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x : ↑(M F)
⊢ ∀ (a b : (j : J) × ↑(F.obj j)),
    Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat)
        a b →
      colimitSMulAux F r a = colimitSMulAux F r b
[PROOFSTEP]
intro x y h
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x✝ : ↑(M F)
x y : (j : J) × ↑(F.obj j)
h :
  Types.Quot.Rel
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
        forget₂ AddGroupCat AddMonCat) ⋙
      forget AddMonCat)
    x y
⊢ colimitSMulAux F r x = colimitSMulAux F r y
[PROOFSTEP]
apply colimitSMulAux_eq_of_rel
[GOAL]
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x✝ : ↑(M F)
x y : (j : J) × ↑(F.obj j)
h :
  Types.Quot.Rel
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
        forget₂ AddGroupCat AddMonCat) ⋙
      forget AddMonCat)
    x y
⊢ Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
[PROOFSTEP]
apply Types.FilteredColimit.rel_of_quot_rel
[GOAL]
case h.a
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r : R
x✝ : ↑(M F)
x y : (j : J) × ↑(F.obj j)
h :
  Types.Quot.Rel
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
        forget₂ AddGroupCat AddMonCat) ⋙
      forget AddMonCat)
    x y
⊢ Types.Quot.Rel (F ⋙ forget (ModuleCat R)) x y
[PROOFSTEP]
exact h
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
x : ↑(M F)
⊢ 1 • x = x
[PROOFSTEP]
refine' Quot.inductionOn x _
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        a
[PROOFSTEP]
clear x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        a
[PROOFSTEP]
intro x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        x =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat))
      x
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        { fst := j, snd := x } =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat))
      { fst := j, snd := x }
[PROOFSTEP]
erw [colimit_smul_mk_eq F 1 ⟨j, x⟩]
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F { fst := { fst := j, snd := x }.fst, snd := 1 • { fst := j, snd := x }.snd } =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat))
      { fst := j, snd := x }
[PROOFSTEP]
simp
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F { fst := j, snd := x } =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat))
      { fst := j, snd := x }
[PROOFSTEP]
rfl
  -- Porting note: writing directly the `Module` instance makes things very slow.
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
x : ↑(M F)
⊢ 1 • x = x
[PROOFSTEP]
refine' Quot.inductionOn x _
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        a
[PROOFSTEP]
clear x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    1 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        a
[PROOFSTEP]
intro x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        x =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat))
      x
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ 1 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        { fst := j, snd := x } =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat))
      { fst := j, snd := x }
[PROOFSTEP]
erw [colimit_smul_mk_eq F 1 ⟨j, x⟩, one_smul]
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F { fst := { fst := j, snd := x }.fst, snd := { fst := j, snd := x }.snd } =
    Quot.mk
      (Types.Quot.Rel
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat))
      { fst := j, snd := x }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
x : ↑(M F)
⊢ (r * s) • x = r • s • x
[PROOFSTEP]
refine' Quot.inductionOn x _
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    (r * s) •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      r •
        s •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a
[PROOFSTEP]
clear x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    (r * s) •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      r •
        s •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a
[PROOFSTEP]
intro x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ (r * s) •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        x =
    r •
      s •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          x
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ (r * s) •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        { fst := j, snd := x } =
    r •
      s •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := x }
[PROOFSTEP]
erw [colimit_smul_mk_eq F (r * s) ⟨j, x⟩, colimit_smul_mk_eq F s ⟨j, x⟩, colimit_smul_mk_eq F r ⟨j, _⟩, mul_smul]
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
r : R
⊢ r • 0 = 0
[PROOFSTEP]
erw [colimit_zero_eq _ (IsFiltered.Nonempty.some : J), colimit_smul_mk_eq, smul_zero]
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
r : R
⊢ M.mk F { fst := { fst := Nonempty.some (_ : Nonempty J), snd := 0 }.fst, snd := 0 } =
    AddMonCat.FilteredColimits.M.mk
      (((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
        forget₂ AddGroupCat AddMonCat)
      { fst := Nonempty.some (_ : Nonempty J), snd := 0 }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
x : ↑(M F)
⊢ 0 • x = 0
[PROOFSTEP]
refine' Quot.inductionOn x _
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    0 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      0
[PROOFSTEP]
clear x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    0 •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      0
[PROOFSTEP]
intro x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ 0 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        x =
    0
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ 0 •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        { fst := j, snd := x } =
    0
[PROOFSTEP]
erw [colimit_smul_mk_eq, zero_smul, colimit_zero_eq _ j]
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝ : MulAction R ↑(M F) := colimitMulAction F
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F { fst := { fst := j, snd := x }.fst, snd := 0 } =
    AddMonCat.FilteredColimits.M.mk
      (((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
        forget₂ AddGroupCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
x : ↑(M F)
⊢ (r + s) • x = r • x + s • x
[PROOFSTEP]
refine' Quot.inductionOn x _
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
x : ↑(M F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    (r + s) •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a +
        s •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a
[PROOFSTEP]
clear x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    (r + s) •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          a =
      r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a +
        s •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a
[PROOFSTEP]
intro x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ (r + s) •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        x =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          x +
      s •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          x
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ (r + s) •
      Quot.mk
        (Types.Quot.Rel
          ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
              forget₂ AddGroupCat AddMonCat) ⋙
            forget AddMonCat))
        { fst := j, snd := x } =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := x } +
      s •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := x }
[PROOFSTEP]
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), CategoryTheory.Functor.map_id, id_apply, id_apply]
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
r s : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F { fst := { fst := j, snd := x }.fst, snd := r • { fst := j, snd := x }.snd + s • { fst := j, snd := x }.snd } =
    AddMonCat.FilteredColimits.M.mk
      (((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
        forget₂ AddGroupCat AddMonCat)
      { fst := j, snd := SMul.smul r { fst := j, snd := x }.snd + SMul.smul s { fst := j, snd := x }.snd }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝¹ : MulAction R ↑(M F) := colimitMulAction F
src✝ : SMulWithZero R ↑(M F) := colimitSMulWithZero F
r : R
x y : ↑(M F)
⊢ r • (x + y) = r • x + r • y
[PROOFSTEP]
refine' Quot.induction_on₂ x y _
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝¹ : MulAction R ↑(M F) := colimitMulAction F
src✝ : SMulWithZero R ↑(M F) := colimitSMulWithZero F
r : R
x y : ↑(M F)
⊢ ∀
    (a b :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    r •
        (Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a +
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            b) =
      r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a +
        r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            b
[PROOFSTEP]
clear x y
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝¹ : MulAction R ↑(M F) := colimitMulAction F
src✝ : SMulWithZero R ↑(M F) := colimitSMulWithZero F
r : R
⊢ ∀
    (a b :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    r •
        (Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a +
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            b) =
      r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a +
        r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            b
[PROOFSTEP]
intro x y
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝¹ : MulAction R ↑(M F) := colimitMulAction F
src✝ : SMulWithZero R ↑(M F) := colimitSMulWithZero F
r : R
x y :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ r •
      (Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          x +
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          y) =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          x +
      r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          y
[PROOFSTEP]
cases' x with i x
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝¹ : MulAction R ↑(M F) := colimitMulAction F
src✝ : SMulWithZero R ↑(M F) := colimitSMulWithZero F
r : R
y :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
i : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    i
⊢ r •
      (Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := i, snd := x } +
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          y) =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := i, snd := x } +
      r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          y
[PROOFSTEP]
cases' y with j y
[GOAL]
case mk.mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝¹ : MulAction R ↑(M F) := colimitMulAction F
src✝ : SMulWithZero R ↑(M F) := colimitSMulWithZero F
r : R
i : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    i
j : J
y :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ r •
      (Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := i, snd := x } +
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := y }) =
    r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := i, snd := x } +
      r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := y }
[PROOFSTEP]
erw [colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j) (IsFiltered.rightToMax i j),
  colimit_smul_mk_eq, smul_add, colimit_smul_mk_eq, colimit_smul_mk_eq,
  colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j) (IsFiltered.rightToMax i j),
  LinearMap.map_smul, LinearMap.map_smul]
[GOAL]
case mk.mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
src✝¹ : MulAction R ↑(M F) := colimitMulAction F
src✝ : SMulWithZero R ↑(M F) := colimitSMulWithZero F
r : R
i : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    i
j : J
y :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ M.mk F
      {
        fst :=
          { fst := IsFiltered.max i j,
              snd :=
                ↑((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                            forget₂ AddGroupCat AddMonCat).map
                        (IsFiltered.leftToMax i j))
                    { fst := i, snd := x }.snd +
                  ↑((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                            forget₂ AddGroupCat AddMonCat).map
                        (IsFiltered.rightToMax i j))
                    { fst := j, snd := y }.snd }.fst,
        snd :=
          r •
              ↑((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                        forget₂ AddGroupCat AddMonCat).map
                    (IsFiltered.leftToMax i j))
                { fst := i, snd := x }.snd +
            r •
              ↑((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                        forget₂ AddGroupCat AddMonCat).map
                    (IsFiltered.rightToMax i j))
                { fst := j, snd := y }.snd } =
    AddMonCat.FilteredColimits.M.mk
      (((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
        forget₂ AddGroupCat AddMonCat)
      { fst := IsFiltered.max i j,
        snd :=
          r • ↑(F.map (IsFiltered.leftToMax i j)) { fst := i, snd := x }.snd +
            r • ↑(F.map (IsFiltered.rightToMax i j)) { fst := j, snd := y }.snd }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
j : J
src✝ : (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat).obj j ⟶
  ((Functor.const J).obj
        (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)).pt).obj
    j :=
  NatTrans.app (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)).ι j
r : R
x : ↑(F.obj j)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat).obj j)),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat).obj j)),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        x
[PROOFSTEP]
erw [colimit_smul_mk_eq F r ⟨j, x⟩]
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
j : J
src✝ : (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat).obj j ⟶
  ((Functor.const J).obj
        (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)).pt).obj
    j :=
  NatTrans.app (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)).ι j
r : R
x : ↑(F.obj j)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat).obj j)),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (r • x) =
    M.mk F { fst := { fst := j, snd := x }.fst, snd := r • { fst := j, snd := x }.snd }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
t : Cocone F
src✝ : (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt ⟶
  ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t).pt :=
  IsColimit.desc
    (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat))
    ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t)
r : R
x : ↑(colimit F)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀
              (x y :
                ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀
                (x y :
                  ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        x
[PROOFSTEP]
refine' Quot.inductionOn x _
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
t : Cocone F
src✝ : (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt ⟶
  ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t).pt :=
  IsColimit.desc
    (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat))
    ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t)
r : R
x : ↑(colimit F)
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀
                (x y :
                  ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀
                  (x y :
                    ↑(AddCommGroupCat.FilteredColimits.colimitCocone
                          (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                  ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
          (Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a)
[PROOFSTEP]
clear x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
t : Cocone F
src✝ : (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt ⟶
  ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t).pt :=
  IsColimit.desc
    (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat))
    ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t)
r : R
⊢ ∀
    (a :
      (j : J) ×
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat).obj
          j),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀
                (x y :
                  ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (r •
          Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀
                  (x y :
                    ↑(AddCommGroupCat.FilteredColimits.colimitCocone
                          (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                  ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
          (Quot.mk
            (Types.Quot.Rel
              ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                  forget₂ AddGroupCat AddMonCat) ⋙
                forget AddMonCat))
            a)
[PROOFSTEP]
intro x
[GOAL]
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
t : Cocone F
src✝ : (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt ⟶
  ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t).pt :=
  IsColimit.desc
    (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat))
    ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t)
r : R
x :
  (j : J) ×
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
            forget₂ AddGroupCat AddMonCat) ⋙
          forget AddMonCat).obj
      j
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀
              (x y :
                ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀
                (x y :
                  ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          x)
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
t : Cocone F
src✝ : (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt ⟶
  ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t).pt :=
  IsColimit.desc
    (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat))
    ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t)
r : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀
              (x y :
                ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (r •
        Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := x }) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀
                (x y :
                  ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := x })
[PROOFSTEP]
erw [colimit_smul_mk_eq]
[GOAL]
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCatMax R
t : Cocone F
src✝ : (AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt ⟶
  ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t).pt :=
  IsColimit.desc
    (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat))
    ((forget₂ (ModuleCat R) AddCommGroupCat).mapCocone t)
r : R
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
          forget₂ AddGroupCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀
              (x y :
                ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (M.mk F { fst := { fst := j, snd := x }.fst, snd := r • { fst := j, snd := x }.snd }) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀
                (x y :
                  ↑(AddCommGroupCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCatMax R) AddCommGroupCat)).pt),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (Quot.mk
          (Types.Quot.Rel
            ((((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                forget₂ AddGroupCat AddMonCat) ⋙
              forget AddMonCat))
          { fst := j, snd := x })
[PROOFSTEP]
exact LinearMap.map_smul (t.ι.app j) r x
