awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m = { app := fun (X : Cᵒᵖ) ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ }
have h : ∀ (X : Cᵒᵖ), m.app X = Hom.app { app := fun (X : Cᵒᵖ) ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := sorry } X
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
X : Cᵒᵖ
⊢ m.app X = Hom.app { app := fun (X : Cᵒᵖ) ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ } X
have h : ∀ (j : J), m.app X ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
Tactic: apply (hc X).uniq ((evaluation R X).mapCone s)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
X : Cᵒᵖ
j : J
⊢ m.app X ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
have h : m.app X ≫ (c.π.app j).app X = (s.π.app j).app X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
X : Cᵒᵖ
j : J
⊢ m.app X ≫ (c.π.app j).app X = (s.π.app j).app X
have h : m.app X ≫ (c.π.app j).app X = (m ≫ c.π.app j).app X
Tactic: rw [← hm, comp_app]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
X : Cᵒᵖ
j : J
h : m.app X ≫ (c.π.app j).app X = (m ≫ c.π.app j).app X
⊢ m.app X ≫ (c.π.app j).app X = (s.π.app j).app X
have h₁ : m.app X ≫ (c.π.app j).app X = m.app X ≫ (c.π.app j).app X
Tactic: rw [← hm, comp_app]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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))
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ HasLimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
have change : HasLimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
Tactic: change HasLimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (R.map f).hom)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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))
X : Cᵒᵖ
⊢ Eq (α :=
    limit (F ⋙ evaluation R X) ⟶
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (limit (F ⋙ evaluation R X)))
    (CategoryStruct.comp (Y := limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
      (limMap (F.whiskerLeft (restriction R (𝟙 X))) :
        limit (F ⋙ evaluation R X) ⟶
          limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
      (Iso.inv (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
        limit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) ⟶
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj (limit (F ⋙ evaluation R X))))
    (Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))))
have rw : Eq (α :=
  limit (F ⋙ evaluation R X) ⟶ limit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
  (limMap (F.whiskerLeft (restriction R (𝟙 X))) :
    limit (F ⋙ evaluation R X) ⟶ limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
  (Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) sorry (limit (F ⋙ evaluation R X))) ≫
      Iso.hom (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
    limit (F ⋙ evaluation R X) ⟶
      limit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
Tactic: rw [← cancel_mono (preservesLimitIso _ _).hom, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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))
X : Cᵒᵖ
⊢ Eq (α :=
    limit (F ⋙ evaluation R X) ⟶
      limit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
    (limMap (F.whiskerLeft (restriction R (𝟙 X))) :
      limit (F ⋙ evaluation R X) ⟶
        limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
    (Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))) ≫
        Iso.hom (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
      limit (F ⋙ evaluation R X) ⟶
        limit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
have w : ∀ (j : J),
  Eq (α :=
    limit (F ⋙ evaluation R X) ⟶ (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
      (limMap (F.whiskerLeft (restriction R (𝟙 X))))
      (limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j))
    (CategoryStruct.comp (Y := limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
      (Iso.inv (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) sorry (limit (F ⋙ evaluation R X))) ≫
          Iso.hom (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)) :
        limit (F ⋙ evaluation R X) ⟶
          limit ((F ⋙ evaluation R X) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))))
      (limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j :
        limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) ⟶
          (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).obj j))
Tactic: apply limit.hom_ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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))
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := limit (F ⋙ evaluation R X) ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((F.obj j).obj Y))
    (CategoryStruct.comp (Y := (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (limit (F ⋙ evaluation R Y)))
      (CategoryStruct.comp (Y := limit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
        (limMap (F.whiskerLeft (restriction R f)) :
          limit (F ⋙ evaluation R X) ⟶
            limit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
        (Iso.inv (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)) :
          limit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) ⟶
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (limit (F ⋙ evaluation R Y))))
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (limit.π (F ⋙ evaluation R Y) j)))
    (limit.π (F ⋙ evaluation R X) j ≫ (F.obj j).map f)
have simp : Eq (α := limit (F ⋙ evaluation R X) ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((F.obj j).obj Y))
  (CategoryStruct.comp (Y := limit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
    (limMap (F.whiskerLeft (restriction R f)))
    (limit.π ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) j))
  (limit.π (F ⋙ evaluation R X) j ≫ (F.obj j).map f)
Tactic: simp only [assoc, preservesLimitIso_inv_π]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits (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 : 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))
j j' : J
f : j ⟶ j'
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (limitPresheafOfModules F)) j ⟶ F.obj j')
    (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (limitPresheafOfModules F)) f ≫
      { app := fun (X : Cᵒᵖ) ↦ limit.π (F ⋙ evaluation R X) j', naturality := ⋯ })
    ({ app := fun (X : Cᵒᵖ) ↦ limit.π (F ⋙ evaluation R X) j, naturality := ⋯ } ≫ F.map f)
have h : ∀ (X : Cᵒᵖ),
  Eq (α := (Functor.obj (Functor.obj (Functor.const J) (limitPresheafOfModules F)) j).obj X ⟶ (F.obj j').obj X)
    (Hom.app
      (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (limitPresheafOfModules F)) f ≫
        { app := fun (X : Cᵒᵖ) ↦ limit.π (F ⋙ evaluation R X) j', naturality := sorry })
      X)
    (Hom.app ({ app := fun (X : Cᵒᵖ) ↦ limit.π (F ⋙ evaluation R X) j, naturality := sorry } ≫ F.map f) X)
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ Y₁ X₂ Y₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁ Y₂)
    (x ⊗ₘ x_1) (x ▷ X₂ ≫ Y₁ ◁ x_1)
have h : ∀ (X : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂).obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁ Y₂).obj X)
    (Hom.app (x ⊗ₘ x_1) X) (Hom.app (x ▷ X₂ ≫ Y₁ ◁ x_1) X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
x x_1 :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
⊢ 𝟙 x ⊗ₘ 𝟙 x_1 = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
have h : ∀ (X : Cᵒᵖ), Hom.app (𝟙 x ⊗ₘ 𝟙 x_1) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ Y₁ Z₁ X₂ Y₂ Z₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : Y₁ ⟶ Z₁
x_3 : Y₂ ⟶ Z₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Z₁ Z₂)
    ((x ⊗ₘ x_1) ≫ (x_2 ⊗ₘ x_3)) (x ≫ x_2 ⊗ₘ x_1 ≫ x_3)
have h : ∀ (X : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂).obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Z₁ Z₂).obj X)
    (Hom.app ((x ⊗ₘ x_1) ≫ (x_2 ⊗ₘ x_3)) X) (Hom.app (x ≫ x_2 ⊗ₘ x_1 ≫ x_3) X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
⊢ M₁ ◁ 𝟙 M₂ = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) M₁ M₂)
have h : ∀ (X : Cᵒᵖ), Hom.app (M₁ ◁ 𝟙 M₂) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) M₁ M₂)) X
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
x x_1 :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
⊢ 𝟙 x ▷ x_1 = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
have h : ∀ (X : Cᵒᵖ), Hom.app (𝟙 x ▷ x_1) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X
Tactic: ext1 X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ X₂ X₃ Y₁ Y₂ Y₃ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : X₃ ⟶ Y₃
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂)
        X₃ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₂ Y₃))
    (((x ⊗ₘ x_1) ⊗ₘ x_2) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (x ⊗ₘ x_1 ⊗ₘ x_2))
have h : ∀ (X : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂)
            X₃).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₂ Y₃)).obj
        X)
    (Hom.app (((x ⊗ₘ x_1) ⊗ₘ x_2) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) X) (Hom.app (Iso.hom (α_ X₁ X₂ X₃) ≫ (x ⊗ₘ x_1 ⊗ₘ x_2)) X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X Y :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X ⟶ Y
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
        ((𝟙_
            (PresheafOfModules
              (R ⋙
                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier))))
          (𝒞 := instCategory))
        X ⟶
      Y)
    ((𝟙_
            (PresheafOfModules
              (R ⋙
                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier))))
          (𝒞 := instCategory) ◁
        x ≫
      Iso.hom (λ_ Y))
    (Iso.hom (λ_ X) ≫ x)
have h : ∀ (X_1 : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
            ((𝟙_
                (PresheafOfModules
                  (R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                      (CD := RingCat.carrier))))
              (𝒞 := instCategory))
            X).obj
        X_1 ⟶
      Y.obj X_1)
    (Hom.app
      ((𝟙_
              (PresheafOfModules
                (R ⋙
                  forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                    (CD := RingCat.carrier))))
            (𝒞 := instCategory) ◁
          x ≫
        Iso.hom (λ_ Y))
      X_1)
    (Hom.app (Iso.hom (λ_ X) ≫ x) X_1)
Tactic: ext1