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)
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 ≫
      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:
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)
X Y : J
f : X ⟶ Y
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 := ⋯ }) X_1)
      (Hom.app
        ({ app := fun (X_2 : Cᵒᵖ) ↦ colimit.ι (F ⋙ evaluation R X_2) X, naturality := ⋯ } ≫
          CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimitPresheafOfModules F)) f)
        X_1)
⊢ 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)

Tactic:
ext1 X
-- 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_1 Y : J
f : X_1 ⟶ Y
X : Cᵒᵖ
⊢ Eq (α := (F.obj X_1).obj X ⟶ (Functor.obj (Functor.obj (Functor.const J) (colimitPresheafOfModules F)) Y).obj X)
    (Hom.app (F.map f ≫ { app := fun (X : Cᵒᵖ) ↦ colimit.ι (F ⋙ evaluation R X) Y, naturality := ⋯ }) X)
    (Hom.app
      ({ app := fun (X : Cᵒᵖ) ↦ colimit.ι (F ⋙ evaluation R X) X_1, naturality := ⋯ } ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimitPresheafOfModules F)) f)
      X)

Tactic:
simpa using colimit.w (F ⋙ evaluation R X) f

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.w
-- 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)
⊢ HasColimit F

Tactic:
⟨_, isColimitColimitCocone F⟩

Premises used: Nonempty.intro, PresheafOfModules.isColimitColimitCocone, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- 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ᵒᵖ
⊢ PreservesColimit F (evaluation R X)

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

Premises used: CategoryTheory.Limits.colimit.isColimit, PresheafOfModules.isColimitColimitCocone, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- 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)
inst_4 :
  ∀ (X : Cᵒᵖ),
    PreservesColimit F
      (evaluation R X ⋙
        forget₂ (ModuleCat.{v, u} (↑(R.obj X) : Type u)) (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) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
⊢ PreservesColimit F (toPresheaf R)

Tactic:
preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F)
    (Limits.evaluationJointlyReflectsColimits _
      (fun X => isColimitOfPreserves (evaluation R X ⋙ forget₂ _ AddCommGrpCat)
        (isColimitColimitCocone F)))

Premises used: PresheafOfModules.evaluation, CategoryTheory.Limits.evaluationJointlyReflectsColimits, ModuleCat, CategoryTheory.Functor.comp, PresheafOfModules.isColimitColimitCocone, CategoryTheory.forget₂, AddCommGrpCat, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone, RingCat.carrier, CategoryTheory.Functor.obj, 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
⊢ HasFiniteColimits (PresheafOfModules.{v, v₁, u₁, u} R)

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteColimits.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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₂
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))
⊢ g₁ = g₂

Tactic:
ext X m₂
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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)
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))
⊢ 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:
obtain ⟨m₁, rfl⟩ := hf m₂

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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))
        ((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:
ConcreteCategory.congr_hom ((evaluation R X ⋙ forget _).congr_map hg) m₁

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.comp, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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))
        ((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:
exact ConcreteCategory.congr_hom ((evaluation R X ⋙ forget _).congr_map hg) m₁

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.comp, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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
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))
⊢ g₁ = g₂

Tactic:
ext X m
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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
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:
hf (ConcreteCategory.congr_hom ((evaluation R X ⋙ forget _).congr_map hg) m)
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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
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:
exact hf (ConcreteCategory.congr_hom ((evaluation R X ⋙ forget _).congr_map hg) m)

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.comp, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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ᵒᵖ
⊢ Epi (f.app X)

Tactic:
inferInstanceAs (Epi ((evaluation R X).map f))

Premises used: _private.0.PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp._proof_1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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ᵒᵖ
⊢ Mono (f.app X)

Tactic:
inferInstanceAs (Mono ((evaluation R X).map f))

Premises used: _private.0.PresheafOfModules.instMonoModuleCatCarrierObjOppositeRingCatApp._proof_1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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ᵒᵖ
rw : Epi (f.app X)
⊢ 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))

Tactic:
rw [← ModuleCat.epi_iff_surjective]

Premises used: ModuleCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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ᵒᵖ
⊢ Epi (f.app X)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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ᵒᵖ
rw : Mono (f.app X)
⊢ 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))

Tactic:
rw [← ModuleCat.mono_iff_injective]

Premises used: ModuleCat.mono_iff_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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ᵒᵖ
⊢ Mono (f.app X)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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₂
⊢ 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))

Tactic:
⟨fun _ ↦ surjective_of_epi f, epi_of_surjective⟩

Premises used: PresheafOfModules.epi_of_surjective, PresheafOfModules.surjective_of_epi, Iff.intro
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
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₂
⊢ 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))

Tactic:
⟨fun _ ↦ injective_of_mono f, mono_of_injective⟩

Premises used: PresheafOfModules.injective_of_mono, PresheafOfModules.mono_of_injective, Iff.intro
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
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)
⊢ ∀ (X : Cᵒᵖ),
    Eq (α :=
      Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X) ⟶
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj
          (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 (𝟙 X)) :
                (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (F.obj X))
              x)))
      ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app
        (Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)))

Tactic:
aesop