awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
⊢ ∀ (j : J),
    Eq (α :=
      Functor.obj
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
          j ⟶
        colimit
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
      (CategoryStruct.comp (Y :=
        colimit
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
        (colimit.ι
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
          j)
        (colimMap
          {
            app := fun (j : J) ↦
              ((F.obj j).smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj (F.obj j))) 1,
            naturality := ⋯ }))
      (CategoryStruct.comp (Y :=
        colimit
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
        (colimit.ι
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
          j)
        1)

Tactic:
simp +instances
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
⊢ ∀ (j : J),
    Eq (α :=
      Functor.obj
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
          j ⟶
        colimit
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
      (CategoryStruct.comp (Y :=
        colimit
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
        (colimit.ι
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
          j)
        (colimMap
          {
            app := fun (j : J) ↦
              ((F.obj j).smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj (F.obj j))) 0,
            naturality := ⋯ }))
      (CategoryStruct.comp (Y :=
        colimit
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
        (colimit.ι
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
          j)
        0)

Tactic:
simp +instances
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
r : R
j : J
⊢ Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (↑s.pt : Type w'))
      (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))
      ((s.pt.smul : (a : R) → End (AddCommGrpCat.of (↑s.pt : Type w'))) r))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (↑(F.obj j) : Type w'))
      (((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) r)
      (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w'))))

Tactic:
smul_naturality (s.ι.app j) r

Premises used: AddMonoidHomClass.toAddMonoidHom, ModuleCat.smul_naturality, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
r : R
j : J
⊢ Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (↑s.pt : Type w'))
      (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))
      ((s.pt.smul : (a : R) → End (AddCommGrpCat.of (↑s.pt : Type w'))) r))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (↑(F.obj j) : Type w'))
      (((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) r)
      (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w'))))

Tactic:
exact smul_naturality (s.ι.app j) r

Premises used: ModuleCat.smul_naturality, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
j : J
⊢ Eq (α :=
    Functor.obj
        (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
          (CD := AddCommGrpCat.carrier))
        (F.obj j) ⟶
      Functor.obj
        (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
          (CD := AddCommGrpCat.carrier))
        s.pt)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
      ((colimitCocone F).ι.app j ≫
        homMk
          (colimit.desc
            (F ⋙
              forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
                (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
            (Functor.mapCocone
              (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
                (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
              s))
          ⋯))
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
      (s.ι.app j))

Tactic:
colimit.ι_desc ((forget₂ _ AddCommGrpCat).mapCocone s) j

Premises used: LinearMap.toAddMonoidHom, CategoryTheory.Functor.mapCocone, CategoryTheory.forget₂, CategoryTheory.Limits.colimit.ι_desc, AddCommGrpCat
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
j : J
⊢ Eq (α :=
    Functor.obj
        (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
          (CD := AddCommGrpCat.carrier))
        (F.obj j) ⟶
      Functor.obj
        (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
          (CD := AddCommGrpCat.carrier))
        s.pt)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
      ((colimitCocone F).ι.app j ≫
        homMk
          (colimit.desc
            (F ⋙
              forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
                (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
            (Functor.mapCocone
              (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
                (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
              s))
          ⋯))
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
      (s.ι.app j))

Tactic:
exact colimit.ι_desc ((forget₂ _ AddCommGrpCat).mapCocone s) j

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.forget₂, CategoryTheory.Limits.colimit.ι_desc, AddCommGrpCat
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
a :
  Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y :=
      colimit
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
      (colimit.ι
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
        j)
      (AddCommGrpCat.ofHom (↑(Hom.hom m) : (↑(mkOfSMul' (coconePointSMul F)) : Type w') →+ (↑s.pt : Type w'))))
    (AddCommGrpCat.ofHom (↑(Hom.hom ((colimitCocone F).ι.app j ≫ m)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))
⊢ Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y :=
      colimit
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
      (colimit.ι
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
        j)
      (AddCommGrpCat.ofHom (↑(Hom.hom m) : (↑(mkOfSMul' (coconePointSMul F)) : Type w') →+ (↑s.pt : Type w'))))
    (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))

Tactic:
rw [← hm]
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y :=
      colimit
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
      (colimit.ι
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
        j)
      (AddCommGrpCat.ofHom (↑(Hom.hom m) : (↑(mkOfSMul' (coconePointSMul F)) : Type w') →+ (↑s.pt : Type w'))))
    (AddCommGrpCat.ofHom (↑(Hom.hom ((colimitCocone F).ι.app j ≫ m)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
⊢ HasColimit F

Tactic:
⟨_, isColimitColimitCocone F⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, ModuleCat.HasColimit.isColimitColimitCocone
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
⊢ PreservesColimit F
    (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
      (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD :=
      AddCommGrpCat.carrier))

Tactic:
preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F) (colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, ModuleCat.HasColimit.isColimitColimitCocone, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
⊢ ReflectsColimit F
    (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
      (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD :=
      AddCommGrpCat.carrier))

Tactic:
reflectsColimit_of_reflectsIsomorphisms _ _

Premises used: CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
⊢ HasFiniteColimits (ModuleCat.{w', w} R)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type u
inst_2 : Ring R
⊢ HasColimits (ModuleCat R)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type u
inst_2 : Ring R
⊢ HasColimits.{u, u + 1} (ModuleCat R)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type u
inst_2 : Ring R
⊢ HasCoequalizers.{u, u + 1} (ModuleCat R)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type u
inst_2 : Ring R
⊢ PreservesColimits
    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type w
inst_2 : CommRing R
M ι : Type u
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ ∀ (s : Cocone (J := Discrete ι) (C := ModuleCat.{u, w} R) (Discrete.functor fun (x : ι) ↦ of R M)) (j : Discrete ι),
    CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (Functor.const (Discrete ι))
            (Cocone.pt (F := Discrete.functor fun (x : ι) ↦ of R M) (finsuppCocone R M ι)))
          j)
        (NatTrans.app (Cocone.ι (finsuppCocone R M ι)) j)
        (↟((Finsupp.lsum R : (a : ι → M →ₗ[R] (↑s.pt : Type u)) → (ι →₀ M) →ₗ[R] (↑s.pt : Type u)) fun (i : ι) ↦
            Hom.hom (s.ι.app { as := i }))) =
      s.ι.app j

Tactic:
aesop (add simp finsuppCocone)

Premises used: ModuleCat.finsuppCocone
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type w
inst_2 : CommRing R
M ι : Type u
inst_3 : AddCommGroup M
inst_4 : Module R M
s : Cocone (J := Discrete ι) (C := ModuleCat.{u, w} R) (Discrete.functor fun (x : ι) ↦ of R M)
f : Cocone.pt (F := Discrete.functor fun (x : ι) ↦ of R M) (finsuppCocone R M ι) ⟶ s.pt
h : ∀ (j : Discrete ι), NatTrans.app (Cocone.ι (finsuppCocone R M ι)) j ≫ f = s.ι.app j
hf :
  Hom.hom f =
    Hom.hom
      (↟((Finsupp.lsum R : (a : ι → M →ₗ[R] (↑s.pt : Type u)) → (ι →₀ M) →ₗ[R] (↑s.pt : Type u)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))
⊢ f =
    ↟((Finsupp.lsum R : (a : ι → M →ₗ[R] (↑s.pt : Type u)) → (ι →₀ M) →ₗ[R] (↑s.pt : Type u)) fun (i : ι) ↦
        Hom.hom (s.ι.app { as := i }))

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type w
inst_2 : CommRing R
M ι : Type u
inst_3 : AddCommGroup M
inst_4 : Module R M
s : Cocone (J := Discrete ι) (C := ModuleCat.{u, w} R) (Discrete.functor fun (x : ι) ↦ of R M)
f : Cocone.pt (F := Discrete.functor fun (x : ι) ↦ of R M) (finsuppCocone R M ι) ⟶ s.pt
h : ∀ (j : Discrete ι), NatTrans.app (Cocone.ι (finsuppCocone R M ι)) j ≫ f = s.ι.app j
i : ι
x : M
⊢ Eq (α := (↑s.pt : Type u)) ((Hom.hom f ∘ₗ Finsupp.lsingle i : (a : M) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
    ((Hom.hom
              (↟((Finsupp.lsum R : (a : ι → M →ₗ[R] (↑s.pt : Type u)) → (ι →₀ M) →ₗ[R] (↑s.pt : Type u)) fun (i : ι) ↦
                  Hom.hom (s.ι.app { as := i }))) ∘ₗ
            Finsupp.lsingle i :
          (a : M) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))

Tactic:
simpa using congr($(h ⟨i⟩) (x : M))