awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
m : (↑(M.obj (Opposite.op X)) : Type v)
h₁ :
  ∀ (g : (free R).obj (Functor.obj yoneda X) ⟶ M),
    Eq (α := (↑(N.obj (Opposite.op X)) : Type v))
      ((ModuleCat.Hom.hom (f₁.app (Opposite.op X)) :
            (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
          ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ M) → (↑(M.obj (Opposite.op X)) : Type v)) g :
            (↑(M.obj (Opposite.op X)) : Type v)) :
        (↑(N.obj (Opposite.op X)) : Type v))
      ((ModuleCat.Hom.hom (f₂.app (Opposite.op X)) :
            (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
          ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ M) → (↑(M.obj (Opposite.op X)) : Type v)) g :
            (↑(M.obj (Opposite.op X)) : Type v)) :
        (↑(N.obj (Opposite.op X)) : Type v))
⊢ Eq (α := (↑(N.obj (Opposite.op X)) : Type v))
    ((ModuleCat.Hom.hom (f₁.app (Opposite.op X)) :
          (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
        m :
      (↑(N.obj (Opposite.op X)) : Type v))
    ((ModuleCat.Hom.hom (f₂.app (Opposite.op X)) :
          (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
        m :
      (↑(N.obj (Opposite.op X)) : Type v))

Tactic:
obtain ⟨g, rfl⟩ := freeYonedaEquiv.surjective m

Premises used: Equiv.surjective, PresheafOfModules.freeYonedaEquiv, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
g : (free R).obj (Functor.obj yoneda X) ⟶ M
⊢ Eq (α := (↑(N.obj (Opposite.op X)) : Type v))
    ((ModuleCat.Hom.hom (f₁.app (Opposite.op X)) :
          (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
        ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ M) → (↑(M.obj (Opposite.op X)) : Type v)) g :
          (↑(M.obj (Opposite.op X)) : Type v)) :
      (↑(N.obj (Opposite.op X)) : Type v))
    ((ModuleCat.Hom.hom (f₂.app (Opposite.op X)) :
          (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
        ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ M) → (↑(M.obj (Opposite.op X)) : Type v)) g :
          (↑(M.obj (Opposite.op X)) : Type v)) :
      (↑(N.obj (Opposite.op X)) : Type v))

Tactic:
congr_arg freeYonedaEquiv (h _ ⟨X⟩ g)

Premises used: congr_arg, CategoryTheory.ObjectProperty.ofObj.mk, DFunLike.coe, PresheafOfModules.freeYonedaEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
g : (free R).obj (Functor.obj yoneda X) ⟶ M
⊢ Eq (α := (↑(N.obj (Opposite.op X)) : Type v))
    ((ModuleCat.Hom.hom (f₁.app (Opposite.op X)) :
          (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
        ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ M) → (↑(M.obj (Opposite.op X)) : Type v)) g :
          (↑(M.obj (Opposite.op X)) : Type v)) :
      (↑(N.obj (Opposite.op X)) : Type v))
    ((ModuleCat.Hom.hom (f₂.app (Opposite.op X)) :
          (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
        ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ M) → (↑(M.obj (Opposite.op X)) : Type v)) g :
          (↑(M.obj (Opposite.op X)) : Type v)) :
      (↑(N.obj (Opposite.op X)) : Type v))

Tactic:
exact congr_arg freeYonedaEquiv (h _ ⟨X⟩ g)

Premises used: congr_arg, CategoryTheory.ObjectProperty.ofObj.mk, DFunLike.coe, PresheafOfModules.freeYonedaEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
⊢ (freeYoneda R).IsDetecting

Tactic:
(isSeparating R).isDetecting

Premises used: PresheafOfModules.freeYoneda.isSeparating, CategoryTheory.ObjectProperty.IsSeparating.isDetecting
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
C₀ : Type u
inst_1 : SmallCategory C₀
R₀ : C₀ᵒᵖ ⥤ RingCat
⊢ WellPowered.{u, u, u + 1} (PresheafOfModules R₀)

Tactic:
wellPowered_of_isDetecting (freeYoneda.isDetecting R₀)

Premises used: PresheafOfModules.freeYoneda.isDetecting, CategoryTheory.wellPowered_of_isDetecting
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              ModuleCat
                (↑(R.obj
                      (m.fst (β := fun (c : Cᵒᵖ) ↦
                        ((toPresheaf R).obj M ⋙
                              forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                                (CC := AddCommGrpCat.carrier)).obj
                          c))) :
                  Type v)) ↦
          LinearMap (R :=
            (↑(R.obj
                  (m.fst (β := fun (c : Cᵒᵖ) ↦
                    ((toPresheaf R).obj M ⋙
                          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                            AddCommGrpCat.carrier)).obj
                      c))) :
              Type v))
            (RingHom.id
              (↑(R.obj
                    (m.fst (β := fun (c : Cᵒᵖ) ↦
                      ((toPresheaf R).obj M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                              AddCommGrpCat.carrier)).obj
                        c))) :
                Type v))
            (↑x1 : Type v) (↑x2 : Type v))
          (CC := ModuleCat.carrier)
          (m.fromFreeYoneda.app
            (m.fst (β := fun (c : Cᵒᵖ) ↦
              ((toPresheaf R).obj M ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                      AddCommGrpCat.carrier)).obj
                c))) :
        (a : (↑(m.freeYoneda.obj m.fst) : Type v)) → (↑(M.obj m.fst) : Type v))
      (ModuleCat.freeMk
        (𝟙
          (Opposite.unop
            (m.fst (β := fun (c : Cᵒᵖ) ↦
              ((toPresheaf R).obj M ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                      AddCommGrpCat.carrier)).obj
                c))))) =
    m.snd (β := fun (c : Cᵒᵖ) ↦
      ((toPresheaf R).obj M ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier)).obj
        c)

Tactic:
apply freeYonedaEquiv_symm_app

Premises used: PresheafOfModules.freeYonedaEquiv_symm_app
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ M.ιFreeYonedaCoproduct m ≫ M.fromFreeYonedaCoproduct = m.fromFreeYoneda

Tactic:
apply Sigma.ι_desc

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
X : Cᵒᵖ
x : (↑(m.freeYoneda.obj X) : Type u)
⊢ Eq (α := (↑(M.obj X) : 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) (M.fromFreeYonedaCoproduct.app X) :
          (a : (↑(M.freeYonedaCoproduct.obj X) : Type u)) → (↑(M.obj X) : 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) ((M.ιFreeYonedaCoproduct m).app X) :
              (a : (↑(m.freeYoneda.obj X) : Type u)) → (↑(M.freeYonedaCoproduct.obj X) : Type u))
            x :
          (↑(M.freeYonedaCoproduct.obj X) : Type u)) :
      (↑(M.obj X) : 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) (m.fromFreeYoneda.app X) :
          (a : (↑(m.freeYoneda.obj X) : Type u)) → (↑(M.obj X) : Type u))
        x :
      (↑(M.obj X) : Type u))

Tactic:
ConcreteCategory.congr_hom
    ((evaluation R X ⋙ forget _).congr_map (M.ι_fromFreeYonedaCoproduct m)) x

Premises used: Multiset.sum, PresheafOfModules.evaluation, Multiset.foldr, PresheafOfModules.ι_fromFreeYonedaCoproduct, CategoryTheory.Functor.comp, Finsupp.sum, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom, Finset.sum
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
R_1 : CategoryTheory.Functor.{v, v, u, v + 1} C_1ᵒᵖ RingCat
C : Type u
inst_1 : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
⊢ Epi M.fromFreeYonedaCoproduct

Tactic:
epi_of_surjective (fun X m ↦ ⟨M.freeYonedaCoproductMk (M.elementsMk X m),
    M.fromFreeYonedaCoproduct_app_mk (M.elementsMk X m)⟩)

Premises used: PresheafOfModules.epi_of_surjective, PresheafOfModules.elementsMk, Exists.intro, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.freeYonedaCoproductMk
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
⊢ M.toFreeYonedaCoproduct ≫ M.fromFreeYonedaCoproduct = 0

Tactic:
simp [toFreeYonedaCoproduct]

Premises used: PresheafOfModules.toFreeYonedaCoproduct
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
R_1 : CategoryTheory.Functor.{v, v, u, v + 1} C_1ᵒᵖ RingCat
C : Type u
inst_1 : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
S : ShortComplex (PresheafOfModules R) :=
  { X₁ := (kernel M.fromFreeYonedaCoproduct).freeYonedaCoproduct, X₂ := M.freeYonedaCoproduct, X₃ := M,
    f := M.toFreeYonedaCoproduct, g := M.fromFreeYonedaCoproduct, zero := ⋯ }
T : ShortComplex (PresheafOfModules R) :=
  ShortComplex.mk (X₁ := kernel M.fromFreeYonedaCoproduct) (kernel.ι M.fromFreeYonedaCoproduct)
    M.fromFreeYonedaCoproduct ⋯
φ : S ⟶ T :=
  { τ₁ := (kernel M.fromFreeYonedaCoproduct).fromFreeYonedaCoproduct, τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ IsColimit M.freeYonedaCoproductsCokernelCofork

Tactic:
exact ((ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).2
    (T.exact_of_f_is_kernel (kernelIsKernel _))).gIsCokernel

Premises used: Iff.mpr, CategoryTheory.ShortComplex.Exact.gIsCokernel, CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
apply :
  ∀ (j : J),
    (s.pt.map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s))) ≫
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j =
      ((hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f) ≫
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j
⊢ Eq (α := s.pt.obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (c.pt.obj Y))
    (s.pt.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s)))
    ((hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f)

Tactic:
apply (isLimitOfPreserves (ModuleCat.restrictScalars (R.map f).hom) (hc Y)).hom_ext

Premises used: ModuleCat.restrictScalars, CategoryTheory.Functor.map, CategoryTheory.Limits.IsLimit.hom_ext, RingCat.Hom.hom, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f

Tactic:
have h₁ := (c.π.app j).naturality f
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
⊢ (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j

Tactic:
have h₂ := (hc X).fac ((evaluation R X).mapCone s) j
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
rw :
  s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone s).π.app j) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j)
⊢ (s.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s))) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j =
    ((hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j

Tactic:
rw [Functor.mapCone_π_app, assoc, assoc, ← Functor.map_comp, IsLimit.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
dsimp :
  s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((s.π.app j).app Y) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y)
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone s).π.app j) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j)

Tactic:
dsimp at h₁ h₂ ⊢
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ : (hc X).lift ((evaluation R X).mapCone s) ≫ (c.π.app j).app X = (s.π.app j).app X
rw :
  s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((s.π.app j).app Y) =
    (hc X).lift ((evaluation R X).mapCone s) ≫ (c.π.app j).app X ≫ (F.obj j).map f
rw₁ :
  s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((s.π.app j).app Y) =
    (s.π.app j).app X ≫ (F.obj j).map f
rw₂ rw₃ : (s.π.app j).app X ≫ (F.obj j).map f = (s.π.app j).app X ≫ (F.obj j).map f
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((s.π.app j).app Y) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y)

Tactic:
rw [h₁, reassoc_of% h₂, Hom.naturality]

Premises used: PresheafOfModules.Hom.naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
j : J
h :
  ∀ (X : Cᵒᵖ),
    Hom.app ({ app := fun (X : Cᵒᵖ) ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ } ≫ c.π.app j) X =
      (s.π.app j).app X
⊢ { app := fun (X : Cᵒᵖ) ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ } ≫ c.π.app j = s.π.app j

Tactic:
ext1 X
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((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)).sections :
        Type (max u₂ v))
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
j : J
X : Cᵒᵖ
⊢ Hom.app ({ app := fun (X : Cᵒᵖ) ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ } ≫ c.π.app j) X =
    (s.π.app j).app X

Tactic:
(hc X).fac ((evaluation R X).mapCone s) j

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.IsLimit.fac