awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ HasColimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))

Tactic:
⟨_, isColimitOfPreserves (ModuleCat.restrictScalars (R.map f).hom)
    (colimit.isColimit (F ⋙ evaluation R Y))⟩

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, ModuleCat.restrictScalars, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, RingCat.Hom.hom, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
dsimp :
  Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R X)) (colimit.ι (F ⋙ evaluation R X) j)
      (CategoryStruct.comp (Y :=
        colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (colimMap (F.whiskerLeft (restriction R (𝟙 X))) :
          colimit (F ⋙ evaluation R X) ⟶
            colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (Iso.inv
            (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
          colimit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))))
    (colimit.ι (F ⋙ evaluation R X) j ≫
      Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))))
⊢ Eq (α :=
    (F ⋙ evaluation R X).obj j ⟶
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R X)) (colimit.ι (F ⋙ evaluation R X) j)
      (CategoryStruct.comp (Y :=
        colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (colimMap (F.whiskerLeft (restriction R (𝟙 X))) :
          colimit (F ⋙ evaluation R X) ⟶
            colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (Iso.inv
            (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
          colimit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))))
    (colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app (colimit (F ⋙ evaluation R X)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
rw :
  Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    ((F.obj j).map (𝟙 X) ≫
      CategoryStruct.comp (Y :=
        colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (colimit.ι (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j :
          (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj j ⟶
            colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (Iso.inv
            (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
          colimit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X))))
    (colimit.ι (F ⋙ evaluation R X) j ≫
      Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))))
⊢ Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R X)) (colimit.ι (F ⋙ evaluation R X) j)
      (CategoryStruct.comp (Y :=
        colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (colimMap (F.whiskerLeft (restriction R (𝟙 X))) :
          colimit (F ⋙ evaluation R X) ⟶
            colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (Iso.inv
            (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
          colimit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))))
    (colimit.ι (F ⋙ evaluation R X) j ≫
      Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))))

Tactic:
rw [ι_colimMap_assoc, Functor.whiskerLeft_app, restriction_app]

Premises used: CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Functor.whiskerLeft_app, PresheafOfModules.restriction_app
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
erw :
  Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    ((F.obj j).map (𝟙 X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j))
    (colimit.ι (F ⋙ evaluation R X) j ≫
      Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))))
⊢ Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    ((F.obj j).map (𝟙 X) ≫
      CategoryStruct.comp (Y :=
        colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (colimit.ι (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j :
          (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj j ⟶
            colimit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
        (Iso.inv
            (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
          colimit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X))))
    (colimit.ι (F ⋙ evaluation R X) j ≫
      Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))))

Tactic:
erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom)]

Premises used: CategoryTheory.CategoryStruct.id, ModuleCat.restrictScalars, CategoryTheory.Functor.map, RingCat.Hom.hom, CategoryTheory.ι_preservesColimitIso_inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
rw :
  Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app ((F.obj j).obj X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j))
    (Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ ((F.obj j).obj X)) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j))
⊢ Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    ((F.obj j).map (𝟙 X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j))
    (colimit.ι (F ⋙ evaluation R X) j ≫
      Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))))

Tactic:
rw [ModuleCat.restrictScalarsId'App_inv_naturality, map_id]

Premises used: ModuleCat.restrictScalarsId'App_inv_naturality, PresheafOfModules.map_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ Eq (α :=
    (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (colimit (F ⋙ evaluation R X)))
    ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app ((F.obj j).obj X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j))
    (Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ ((F.obj j).obj X)) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
erw :
  Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    ((F.obj j).map (f ≫ g) ≫
      CategoryTheory.Functor.map (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
        (colimit.ι (F ⋙ evaluation R Z) j))
    ((F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        Iso.inv
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))
⊢ Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    ((F.obj j).map (f ≫ g) ≫
      CategoryTheory.Functor.map (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
        (colimit.ι (F ⋙ evaluation R Z) j))
    ((F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            CategoryStruct.comp (Y :=
              colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
              (colimit.ι (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) j :
                (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj j ⟶
                  colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
              (Iso.inv
                  (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)) :
                colimit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) ⟶
                  (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (colimit (F ⋙ evaluation R Z)))) ≫
        Iso.inv
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))

Tactic:
erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map g).hom)]

Premises used: ModuleCat.restrictScalars, CategoryTheory.Functor.map, RingCat.Hom.hom, CategoryTheory.ι_preservesColimitIso_inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
rw :
  Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
        Iso.inv
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F.obj j).obj Z)) ≫
          CategoryTheory.Functor.map (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
            (colimit.ι (F ⋙ evaluation R Z) j))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.obj j).map g ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        Iso.inv
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))
⊢ Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    ((F.obj j).map (f ≫ g) ≫
      CategoryTheory.Functor.map (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
        (colimit.ι (F ⋙ evaluation R Z) j))
    ((F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        Iso.inv
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))

Tactic:
rw [map_comp, ModuleCat.restrictScalarsComp'_inv_app, assoc, assoc,
      Functor.whiskerLeft_app, Functor.whiskerLeft_app, restriction_app, restriction_app]

Premises used: CategoryTheory.Category.assoc, ModuleCat.restrictScalarsComp'_inv_app, CategoryTheory.Functor.whiskerLeft_app, PresheafOfModules.map_comp, PresheafOfModules.restriction_app
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
simp :
  Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
        Iso.inv
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F.obj j).obj Z)) ≫
          CategoryTheory.Functor.map (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
            (colimit.ι (F ⋙ evaluation R Z) j))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
          Iso.inv
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))
⊢ Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
        Iso.inv
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F.obj j).obj Z)) ≫
          CategoryTheory.Functor.map (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
            (colimit.ι (F ⋙ evaluation R Z) j))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.obj j).map g ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        Iso.inv
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))

Tactic:
simp only [Functor.map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
        Iso.inv
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F.obj j).obj Z)) ≫
          CategoryTheory.Functor.map (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
            (colimit.ι (F ⋙ evaluation R Z) j))
    ((F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
          Iso.inv
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
erw :
  Eq (α := (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (colimit (F ⋙ evaluation R Y)))
    ((F.obj j).map f ≫
      CategoryStruct.comp (Y := colimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
        (colimit.ι ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) j :
          ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj j ⟶
            colimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
        (Iso.inv (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)) :
          colimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (colimit (F ⋙ evaluation R Y))))
    ((F.whiskerLeft (restriction R f)).app j ≫
      (colimit.cocone (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))).ι.app j ≫
        Iso.inv (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)))
⊢ Eq (α := (F.obj j).obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (colimit (F ⋙ evaluation R Y)))
    ((F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j))
    (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R X)) (colimit.ι (F ⋙ evaluation R X) j)
      (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
        (colimMap (F.whiskerLeft (restriction R f)) :
          colimit (F ⋙ evaluation R X) ⟶
            colimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
        (Iso.inv (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)) :
          colimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (colimit (F ⋙ evaluation R Y)))))

Tactic:
erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitIso_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.ι_preservesColimitIso_inv