awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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 ≫ 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))))
have 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))) sorry (colimit (F ⋙ evaluation R Z))))
Tactic: erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map g).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 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 ≫ 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))))
have 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))) sorry ((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))) sorry (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]
-- 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 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 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))))
have 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))) sorry ((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))) sorry (colimit (F ⋙ evaluation R Z))))
Tactic: simp only [Functor.map_comp, assoc]
-- 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)
j : J
X Y : Cᵒᵖ
f : X ⟶ 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)))))
have 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)))
Tactic: erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitIso_inv]
-- 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 Y : J
f : X ⟶ Y
⊢ Eq (α := F.obj X ⟶ Functor.obj (Functor.obj (Functor.const J) (colimitPresheafOfModules F)) Y)
    (F.map f ≫ { app := fun (X : Cᵒᵖ) ↦ colimit.ι (F ⋙ evaluation R X) Y, naturality := ⋯ })
    ({ app := fun (X_1 : Cᵒᵖ) ↦ colimit.ι (F ⋙ evaluation R X_1) X, naturality := ⋯ } ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimitPresheafOfModules F)) f)
have h : ∀ (X_1 : Cᵒᵖ),
  Eq (α := (F.obj X).obj X_1 ⟶ (Functor.obj (Functor.obj (Functor.const J) (colimitPresheafOfModules F)) Y).obj X_1)
    (Hom.app (F.map f ≫ { app := fun (X : Cᵒᵖ) ↦ colimit.ι (F ⋙ evaluation R X) Y, naturality := sorry }) X_1)
    (Hom.app
      ({ app := fun (X_2 : Cᵒᵖ) ↦ colimit.ι (F ⋙ evaluation R X_2) X, naturality := sorry } ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimitPresheafOfModules F)) f)
      X_1)
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
hf :
  ∀ ⦃X : Cᵒᵖ⦄,
    Function.Surjective (α := (↑(M₁.obj X) : Type v)) (β := (↑(M₂.obj X) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (f.app X)) :
        (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
Z : PresheafOfModules.{v, v₁, u₁, u} R
g₁ g₂ : M₂ ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
⊢ g₁ = g₂
have h : ∀ (X : Cᵒᵖ) (m₂ : (↑(M₂.obj X) : Type v)),
  Eq (α := (↑(Z.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₁.app X) : (a : (↑(M₂.obj X) : Type v)) → (↑(Z.obj X) : Type v)) m₂ : (↑(Z.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₂.app X) : (a : (↑(M₂.obj X) : Type v)) → (↑(Z.obj X) : Type v)) m₂ : (↑(Z.obj X) : Type v))
Tactic: ext X m₂
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
hf :
  ∀ ⦃X : Cᵒᵖ⦄,
    Function.Surjective (α := (↑(M₁.obj X) : Type v)) (β := (↑(M₂.obj X) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (f.app X)) :
        (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
Z : PresheafOfModules.{v, v₁, u₁, u} R
g₁ g₂ : M₂ ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
X : Cᵒᵖ
m₂ : (↑(M₂.obj X) : Type v)
⊢ Eq (α := (↑(Z.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₁.app X) : (a : (↑(M₂.obj X) : Type v)) → (↑(Z.obj X) : Type v)) m₂ : (↑(Z.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₂.app X) : (a : (↑(M₂.obj X) : Type v)) → (↑(Z.obj X) : Type v)) m₂ : (↑(Z.obj X) : Type v))
have h : ∀ (m₁ : (↑(M₁.obj X) : Type v)),
  Eq (α := (↑(Z.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₁.app X) : (a : (↑(M₂.obj X) : Type v)) → (↑(Z.obj X) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app X) :
              (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
            m₁ :
          (↑(M₂.obj X) : Type v)) :
      (↑(Z.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₂.app X) : (a : (↑(M₂.obj X) : Type v)) → (↑(Z.obj X) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app X) :
              (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
            m₁ :
          (↑(M₂.obj X) : Type v)) :
      (↑(Z.obj X) : Type v))
Tactic: obtain ⟨m₁, rfl⟩ := hf m₂
Cleared hypotheses: m₂
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
hf :
  ∀ ⦃X : Cᵒᵖ⦄,
    Function.Injective (α := (↑(M₁.obj X) : Type v)) (β := (↑(M₂.obj X) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (f.app X)) :
        (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
M : PresheafOfModules.{v, v₁, u₁, u} R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂
have h : ∀ (X : Cᵒᵖ) (m : (↑(M.obj X) : Type v)),
  Eq (α := (↑(M₁.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₁.app X) : (a : (↑(M.obj X) : Type v)) → (↑(M₁.obj X) : Type v)) m : (↑(M₁.obj X) : Type v))
    ((ModuleCat.Hom.hom (g₂.app X) : (a : (↑(M.obj X) : Type v)) → (↑(M₁.obj X) : Type v)) m : (↑(M₁.obj X) : Type v))
Tactic: ext X m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
inst_1 : Epi f
X : Cᵒᵖ
⊢ Function.Surjective (α := (↑(M₁.obj X) : Type v)) (β := (↑(M₂.obj X) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
          LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
            (↑x2 : Type v))
          (CC := ModuleCat.carrier) (f.app X)) :
      (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
have rw : Epi (f.app X)
Tactic: rw [← ModuleCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
inst_1 : Mono f
X : Cᵒᵖ
⊢ Function.Injective (α := (↑(M₁.obj X) : Type v)) (β := (↑(M₂.obj X) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
          LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
            (↑x2 : Type v))
          (CC := ModuleCat.carrier) (f.app X)) :
      (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
have rw : Mono (f.app X)
Tactic: rw [← ModuleCat.mono_iff_injective]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
F : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ (Type u)
G : PresheafOfModules R
φ :
  F ⟶
    G.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ModuleCat.freeDesc
        (↾fun (x : F.obj X) ↦
          ModuleCat.freeMk ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x)) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y)) =
    ModuleCat.freeDesc (φ.app X) ≫ G.map f
have h : ∀ (x : F.obj X),
  Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (X := Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X))
            (ModuleCat.freeDesc
                (↾fun (x : F.obj X) ↦
                  ModuleCat.freeMk ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x)) ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y))) :
          (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
        (ModuleCat.freeMk x) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (ModuleCat.freeDesc (φ.app X) ≫ G.map f) :
          (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
        (ModuleCat.freeMk x) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
F : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ (Type u)
G : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.map f ≫ ↾fun (x : F.obj Y) ↦ ModuleCat.freeMk x) =
    (↾fun (x : F.obj X) ↦ ModuleCat.freeMk x) ≫
      (presheaf (R := R) (freeObj F) ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)).map
        f
have h : ∀ (x : F.obj X),
  TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f ≫ ↾fun (x : F.obj Y) ↦ ModuleCat.freeMk x)) x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : F.obj X) ↦ ModuleCat.freeMk x) ≫
          (presheaf (R := R) (freeObj F) ⋙
                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)).map
            f))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
F : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ (Type u)
G : PresheafOfModules R
ψ : freeObj F ⟶ G
⊢ (fun
          (φ :
            F ⟶
              G.presheaf ⋙
                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)) ↦
        freeObjDesc φ)
      ((fun (ψ : freeObj F ⟶ G) ↦
          freeAdjunctionUnit R F ≫
            Functor.whiskerRight ((toPresheaf R).map ψ)
              (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier)))
        ψ) =
    ψ
have h : ∀ (X : Cᵒᵖ),
  Hom.app
      ((fun
            (φ :
              F ⟶
                G.presheaf ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)) ↦
          freeObjDesc φ)
        ((fun (ψ : freeObj F ⟶ G) ↦
            freeAdjunctionUnit R F ≫
              Functor.whiskerRight ((toPresheaf R).map ψ)
                (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)))
          ψ))
      X =
    ψ.app X
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
F : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ (Type u)
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
⊢ Hom.app
      ((fun
            (φ :
              F ⟶
                G.presheaf ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)) ↦
          freeObjDesc φ)
        ((fun (ψ : freeObj F ⟶ G) ↦
            freeAdjunctionUnit R F ≫
              Functor.whiskerRight ((toPresheaf R).map ψ)
                (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)))
          ψ))
      X =
    ψ.app X
have h : ModuleCat.freeDesc
    (CategoryStruct.comp (Y := (↑(Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)) : Type u))
      (↾fun (x : F.obj X) ↦ ModuleCat.freeMk x)
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app X)) :
          (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) → (↑(G.obj X) : Type u)))) =
  ψ.app X
Tactic: dsimp