awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
N : ModuleCat (↑cR.pt : Type w)
f : M ⟶ M'
g : M' ⟶ (constFunctor cR).obj N
⊢ Eq (α := M ⟶ (constFunctor cR).obj N)
    ((homEquiv hcR hcM : (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
        ((AddEquiv.symm (homEquiv hcR hcM) :
            (a : M ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N)
          (f ≫ g)) :
      M ⟶ (constFunctor cR).obj N)
    ((homEquiv hcR hcM : (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
        (ModuleCat.ofHom (map hcR hcM hcM' f) ≫
          (AddEquiv.symm (homEquiv hcR hcM') :
              (a : M' ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N)
            g) :
      M ⟶ (constFunctor cR).obj N)
have obtain : ∀ (g : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N),
  Eq (α := M ⟶ (constFunctor cR).obj N)
    ((homEquiv hcR hcM : (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
        ((AddEquiv.symm (homEquiv hcR hcM) :
            (a : M ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N)
          (f ≫
            (homEquiv hcR hcM' :
                (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N) → M' ⟶ (constFunctor cR).obj N)
              g)) :
      M ⟶ (constFunctor cR).obj N)
    ((homEquiv hcR hcM : (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
        (ModuleCat.ofHom (map hcR hcM hcM' f) ≫
          (AddEquiv.symm (homEquiv hcR hcM') :
              (a : M' ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N)
            ((homEquiv hcR hcM' :
                (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N) → M' ⟶ (constFunctor cR).obj N)
              g)) :
      M ⟶ (constFunctor cR).obj N)
Tactic: obtain ⟨g, rfl⟩ := (homEquiv hcR hcM').surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
X Y Z : PresheafOfModules R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat (↑cR.pt : Type w))
      (ModuleCat.of (↑cR.pt : Type w)
        (ModuleColimit (cM := colimit.cocone X.presheaf) hcR (colimit.isColimit X.presheaf)))
      (ModuleCat.of (↑cR.pt : Type w)
        (ModuleColimit (cM := colimit.cocone Z.presheaf) hcR (colimit.isColimit Z.presheaf))))
    (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Z.presheaf) (f ≫ g)))
    (CategoryStruct.comp (Y :=
      ModuleCat.of (↑cR.pt : Type w)
        (ModuleColimit (cM := colimit.cocone Y.presheaf) hcR (colimit.isColimit Y.presheaf)))
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Y.presheaf) f))
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y.presheaf) (colimit.isColimit Z.presheaf) g)))
have hf : Eq (α :=
  LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w))
    (↑(ModuleCat.of (↑cR.pt : Type w)
          (ModuleColimit (cM := colimit.cocone X.presheaf) hcR (colimit.isColimit X.presheaf))) :
      Type w)
    (↑(ModuleCat.of (↑cR.pt : Type w)
          (ModuleColimit (cM := colimit.cocone Z.presheaf) hcR (colimit.isColimit Z.presheaf))) :
      Type w))
  (ModuleCat.Hom.hom
    (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Z.presheaf) (f ≫ g))))
  (ModuleCat.Hom.hom
    (CategoryStruct.comp (Y :=
      ModuleCat.of (↑cR.pt : Type w)
        (ModuleColimit (cM := colimit.cocone Y.presheaf) hcR (colimit.isColimit Y.presheaf)))
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Y.presheaf) f))
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y.presheaf) (colimit.isColimit Z.presheaf) g))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ Eq (α := (F ⋙ evaluation R X).obj j ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (s.pt.obj Y))
    (((evaluation R X).mapCocone c).ι.app j ≫
        c.pt.map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) :
      (F ⋙ evaluation R X).obj j ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (s.pt.obj Y))
    (((evaluation R X).mapCocone c).ι.app j ≫ (hc X).desc ((evaluation R X).mapCocone s) ≫ s.pt.map f :
      (F ⋙ evaluation R X).obj j ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (s.pt.obj Y))
have rw : ((evaluation R X).mapCocone c).ι.app j ≫
    c.pt.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
  ((evaluation R X).mapCocone s).ι.app j ≫ s.pt.map f
Tactic: rw [(hc X).fac_assoc ((evaluation R X).mapCocone s) j]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (hypothesis)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone s).ι.app j ≫ s.pt.map f
have h₁ : (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.ι.app j).app Y) =
  (c.ι.app j).app X ≫ (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f
Tactic: have h₁ := (c.ι.app j).naturality f
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (hypothesis)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.ι.app j).app Y) =
    (c.ι.app j).app X ≫ (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone s).ι.app j ≫ s.pt.map f
have h₂ : ∀ (j : J),
  ((evaluation R Y).mapCocone c).ι.app j ≫ (hc Y).desc ((evaluation R Y).mapCocone s) =
    ((evaluation R Y).mapCocone s).ι.app j
Tactic: have h₂ := (hc Y).fac ((evaluation R Y).mapCocone s)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.ι.app j).app Y) =
    (c.ι.app j).app X ≫ (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f
h₂ :
  ∀ (j : J),
    ((evaluation R Y).mapCocone c).ι.app j ≫ (hc Y).desc ((evaluation R Y).mapCocone s) =
      ((evaluation R Y).mapCocone s).ι.app j
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone s).ι.app j ≫ s.pt.map f
have dsimp : (c.ι.app j).app X ≫
    c.pt.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
  (s.ι.app j).app X ≫ s.pt.map f
Tactic: dsimp at h₁ h₂ ⊢
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫ { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ } = s.ι.app j
have h : ∀ (X : Cᵒᵖ),
  Hom.app (c.ι.app j ≫ { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := sorry }) X =
    (s.ι.app j).app X
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m = { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }
have h : ∀ (X : Cᵒᵖ), m.app X = Hom.app { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := sorry } X
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
⊢ m.app X = Hom.app { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ } X
have h : ∀ (j : J), ((evaluation R X).mapCocone c).ι.app j ≫ m.app X = ((evaluation R X).mapCocone s).ι.app j
Tactic: apply (hc X).uniq ((evaluation R X).mapCocone s)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ ((evaluation R X).mapCocone c).ι.app j ≫ m.app X = ((evaluation R X).mapCocone s).ι.app j
have h : (c.ι.app j).app X ≫ m.app X = (s.ι.app j).app X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ (c.ι.app j).app X ≫ m.app X = (s.ι.app j).app X
have h : (c.ι.app j).app X ≫ m.app X = (c.ι.app j ≫ m).app X
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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 ⋙ 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)))
have 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))) sorry (colimit (F ⋙ evaluation R X))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
    (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))))
have 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))) sorry (colimit (F ⋙ evaluation R X))))
Tactic: rw [ι_colimMap_assoc, Functor.whiskerLeft_app, restriction_app]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
    ((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))))
have 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))) sorry (colimit (F ⋙ evaluation R X))))
Tactic: erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom)]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
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)))
    ((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))))
have 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))) sorry).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))) sorry ((F.obj j).obj X)) ≫
    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j))
Tactic: rw [ModuleCat.restrictScalarsId'App_inv_naturality, map_id]