[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


[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
⊢ Inhabited (ColimitType F)
[PROOFSTEP]
dsimp [ColimitType]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
⊢ Inhabited (Quotient (colimitSetoid F))
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
⊢ Monoid (ColimitType F)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case w.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
[PROOFSTEP]
apply Relation.map
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(coconeMorphism F j) x
[PROOFSTEP]
rw [← cocone_naturality F f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(F.map f ≫ coconeMorphism F j') x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), Setoid.r a b → descFunLift F s a = descFunLift F s b
[PROOFSTEP]
intro x y r
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction' r with _ _ _ _ h _ _ _ _ _ h₁ h₂ _ _ f x _ _ _ _ _ _ _ _ h _ _ _ _ h
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
h : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
h : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
h₁ : descFunLift F s x✝² = descFunLift F s y✝
h₂ : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
h₁ : descFunLift F s x✝² = descFunLift F s y✝
h₂ : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x✝ y : Prequotient F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j'✝ (↑(F.map f) x)) = descFunLift F s (Prequotient.of j✝ x)
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x✝ y : Prequotient F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j'✝ (↑(F.map f) x)) = descFunLift F s (Prequotient.of j✝ x)
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ y✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (x✝ * y✝)) = descFunLift F s (mul (Prequotient.of j✝ x✝) (Prequotient.of j✝ y✝))
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ y✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (x✝ * y✝)) = descFunLift F s (mul (Prequotient.of j✝ x✝) (Prequotient.of j✝ y✝))
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 1) = descFunLift F s one
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 1) = descFunLift F s one
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
h : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x'✝ y✝)
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
h : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x'✝ y✝)
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
h : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x✝¹ y'✝)
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
h : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x✝¹ y'✝)
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (mul (mul x✝ y✝) z✝) = descFunLift F s (mul x✝ (mul y✝ z✝))
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (mul (mul x✝ y✝) z✝) = descFunLift F s (mul x✝ (mul y✝ z✝))
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul one x✝) = descFunLift F s x✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul one x✝) = descFunLift F s x✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul x✝ one) = descFunLift F s x✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul x✝ one) = descFunLift F s x✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
h : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
exact h.symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
h₁ : descFunLift F s x✝² = descFunLift F s y✝
h₂ : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
exact h₁.trans h₂
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x✝ y : Prequotient F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : ↑(F.obj j✝)
⊢ ↑(NatTrans.app s.ι j'✝) (↑(F.map f) x) = ↑(NatTrans.app s.ι j✝) x
[PROOFSTEP]
exact s.w_apply f x
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
h : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s x✝¹ * descFunLift F s y✝ = descFunLift F s x'✝ * descFunLift F s y✝
[PROOFSTEP]
rw [h]
  -- mul_2
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
h : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s x✝¹ * descFunLift F s y✝ = descFunLift F s x✝¹ * descFunLift F s y'✝
[PROOFSTEP]
rw [h]
  -- mul_assoc
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s x✝ * descFunLift F s y✝ * descFunLift F s z✝ =
    descFunLift F s x✝ * (descFunLift F s y✝ * descFunLift F s z✝)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : ↑(colimit F)
⊢ OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y
[PROOFSTEP]
induction x using Quot.inductionOn
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
y : ↑(colimit F)
a✝ : Prequotient F
⊢ OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝ * y) =
    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝) *
      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y
[PROOFSTEP]
induction y using Quot.inductionOn
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : Prequotient F
⊢ OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) }
      (Quot.mk Setoid.r a✝¹ * Quot.mk Setoid.r a✝) =
    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝¹) *
      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝)
[PROOFSTEP]
dsimp [descFun]
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : Prequotient F
⊢ Quot.lift (descFunLift F s) (_ : ∀ (x y : Prequotient F), Setoid.r x y → descFunLift F s x = descFunLift F s y)
      (Quot.mk Setoid.r a✝¹ * Quot.mk Setoid.r a✝) =
    descFunLift F s a✝¹ * descFunLift F s a✝
[PROOFSTEP]
rw [← quot_mul]
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : Prequotient F
⊢ Quot.lift (descFunLift F s) (_ : ∀ (x y : Prequotient F), Setoid.r x y → descFunLift F s x = descFunLift F s y)
      (Quot.mk Setoid.r (mul a✝¹ a✝)) =
    descFunLift F s a✝¹ * descFunLift F s a✝
[PROOFSTEP]
simp only [descFunLift]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => descMorphism F s) s
[PROOFSTEP]
ext x
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ ↑m x = ↑((fun s => descMorphism F s) s) x
[PROOFSTEP]
induction' x using Quot.inductionOn with x
[GOAL]
case w.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction' x with j x x y hx hy
[GOAL]
case w.h.of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]
change _ = s.ι.app j _
[GOAL]
case w.h.of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑(NatTrans.app s.ι j) x
[PROOFSTEP]
rw [← w j]
[GOAL]
case w.h.of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑(NatTrans.app (colimitCocone F).ι j ≫ m) x
[PROOFSTEP]
rfl
[GOAL]
case w.h.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r one) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r one)
[PROOFSTEP]
rw [quot_one, map_one]
[GOAL]
case w.h.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ 1 = ↑((fun s => descMorphism F s) s) 1
[PROOFSTEP]
rfl
[GOAL]
case w.h.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
hx : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
hy : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (mul x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (mul x y))
[PROOFSTEP]
rw [quot_mul, map_mul, hx, hy]
[GOAL]
case w.h.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
hx : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
hy : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x) * ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y) =
    ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x * Quot.mk Setoid.r y)
[PROOFSTEP]
dsimp [descMorphism, FunLike.coe, descFun]
[GOAL]
case w.h.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
hx : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
hy : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ descFunLift F s x * descFunLift F s y =
    Quot.lift (descFunLift F s) (_ : ∀ (x y : Prequotient F), Setoid.r x y → descFunLift F s x = descFunLift F s y)
      (Quot.mk Setoid.r x * Quot.mk Setoid.r y)
[PROOFSTEP]
simp only [← quot_mul, descFunLift]


[GOAL]
X Y : MonCat
⊢ FunLike (↑X →* ↑Y) ↑X fun x => ↑Y
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
G : Type u_1
inst✝ : Group G
⊢ Group ↑(of G)
[PROOFSTEP]
assumption
[GOAL]
⊢ ConcreteCategory CommMonCat
[PROOFSTEP]
dsimp only [CommMonCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommMonoid)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : CommMonCat
⊢ FunLike (↑X →* ↑Y) ↑X fun x => ↑Y
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
R S : MonCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
[GOAL]
R S : CommMonCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
  -- We verify that when constructing a morphism in `CommMonCat`,
  -- when we construct the `toFun` field, the types are presented as `↑R`.
[GOAL]
R : CommMonCat
x : ↑R
⊢ ↑R
[PROOFSTEP]
match_target (R : Type u)
[GOAL]
R : CommMonCat
x : ↑R
⊢ ↑R
[PROOFSTEP]
guard_hyp x : (R : Type u)
[GOAL]
R : CommMonCat
x : ↑R
⊢ ↑R
[PROOFSTEP]
exact x * x
[GOAL]
R : CommMonCat
⊢ (fun x => x * x) 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : CommMonCat
x y : ↑R
⊢ OneHom.toFun { toFun := fun x => x * x, map_one' := (_ : 1 * 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => x * x, map_one' := (_ : 1 * 1 = 1) } x *
      OneHom.toFun { toFun := fun x => x * x, map_one' := (_ : 1 * 1 = 1) } y
[PROOFSTEP]
dsimp
[GOAL]
R : CommMonCat
x y : ↑R
⊢ x * y * (x * y) = x * x * (y * y)
[PROOFSTEP]
rw [mul_assoc x y (x * y), ← mul_assoc y x y, mul_comm y x, mul_assoc, mul_assoc]
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget MonCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (by aesop)
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
⊢ ∀ (x y : ↑X), Equiv.toFun i.toEquiv (x * y) = Equiv.toFun i.toEquiv x * Equiv.toFun i.toEquiv y
[PROOFSTEP]
aesop
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
e : ↑X ≃* ↑Y := { toEquiv := i.toEquiv, map_mul' := (_ : ∀ (x_1 y : ↑X), ↑f (x_1 * y) = ↑f x_1 * ↑f y) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toMonCatIso
[GOAL]
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommMonCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f))
[GOAL]
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
e : ↑X ≃* ↑Y :=
  { toEquiv := i.toEquiv,
    map_mul' :=
      (_ :
        ∀ (a b : ↑X),
          ↑(let_fun this := f;
                this)
              (a * b) =
            ↑(let_fun this := f;
                  this)
                a *
              ↑(let_fun this := f;
                  this)
                b) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toCommMonCatIso