awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) X
        ((𝟙_
            (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)) ⟶
      Y)
    (x ▷
        (𝟙_
            (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) ≫
      Iso.hom (ρ_ Y))
    (Iso.hom (ρ_ X) ≫ x)
have h : ∀ (X_1 : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X
            ((𝟙_
                (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))).obj
        X_1 ⟶
      Y.obj X_1)
    (Hom.app
      (x ▷
          (𝟙_
              (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) ≫
        Iso.hom (ρ_ Y))
      X_1)
    (Hom.app (Iso.hom (ρ_ X) ≫ x) X_1)
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 x_2 x_3 :
  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))
⊢ Iso.hom (α_ x x_1 x_2) ▷ x_3 ≫
      Iso.hom (α_ x (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2) x_3) ≫ x ◁ Iso.hom (α_ x_1 x_2 x_3) =
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1) x_2 x_3) ≫
      Iso.hom (α_ x x_1 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x_3))
have h : ∀ (X : Cᵒᵖ),
  Hom.app
      (Iso.hom (α_ x x_1 x_2) ▷ x_3 ≫
        Iso.hom (α_ x (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2) x_3) ≫
          x ◁ Iso.hom (α_ x_1 x_2 x_3))
      X =
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1) x_2 x_3) ≫
          Iso.hom (α_ x x_1 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x_3))).app
      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))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x
          ((𝟙_
              (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_1 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
    (Iso.hom
        (α_ x
          ((𝟙_
              (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_1) ≫
      x ◁ Iso.hom (λ_ x_1))
    (Iso.hom (ρ_ x) ▷ x_1)
have h : ∀ (X : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x
              ((𝟙_
                  (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_1).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X)
    (Hom.app
      (Iso.hom
          (α_ x
            ((𝟙_
                (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_1) ≫
        x ◁ Iso.hom (λ_ x_1))
      X)
    (Hom.app (Iso.hom (ρ_ 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 x_1 x_2 :
  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_3 : x_1 ⟶ x_2
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)
    (x ◁ x_3 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯))
    (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ≫ x_3 ▷ x)
have h : ∀ (X : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x).obj X)
    (Hom.app (x ◁ x_3 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) sorry)) X)
    (Hom.app (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) sorry) ≫ x_3 ▷ x) X)
Tactic: ext : 1
-- 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
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))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X x_1 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 Y)
    (x ▷ x_1 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (Y.obj X) (x_1.obj X)) ⋯))
    (Iso.hom (isoMk (fun (X_1 : Cᵒᵖ) ↦ β_ (X.obj X_1) (x_1.obj X_1)) ⋯) ≫ x_1 ◁ x)
have h : ∀ (X_1 : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X x_1).obj X_1 ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 Y).obj X_1)
    (Hom.app (x ▷ x_1 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (Y.obj X) (x_1.obj X)) sorry)) X_1)
    (Hom.app (Iso.hom (isoMk (fun (X_2 : Cᵒᵖ) ↦ β_ (X.obj X_2) (x_1.obj X_2)) sorry) ≫ x_1 ◁ x) X_1)
Tactic: ext : 1
-- 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 x_2 :
  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))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
        x_2 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x))
    (Iso.hom (α_ x x_1 x_2) ≫
      Iso.hom
          (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2).obj X))
            ⋯) ≫
        Iso.hom (α_ x_1 x_2 x))
    (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ▷ x_2 ≫
      Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯))
have h : ∀ (X : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
            x_2).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)).obj
        X)
    (Hom.app
      (Iso.hom (α_ x x_1 x_2) ≫
        Iso.hom
            (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2).obj X))
              sorry) ≫
          Iso.hom (α_ x_1 x_2 x))
      X)
    (Hom.app
      (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) sorry) ▷ x_2 ≫
        Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) sorry))
      X)
Tactic: ext : 1
-- 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 x_2 :
  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))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2) ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)
        x_1)
    (Iso.inv (α_ x x_1 x_2) ≫
      Iso.hom
          (isoMk (fun (X : Cᵒᵖ) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X) (x_2.obj X))
            ⋯) ≫
        Iso.inv (α_ x_2 x x_1))
    (x ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x_2.obj X)) ⋯) ≫
      Iso.inv (α_ x x_2 x_1) ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯) ▷ x_1)
have h : ∀ (X : Cᵒᵖ),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2)).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)
            x_1).obj
        X)
    (Hom.app
      (Iso.inv (α_ x x_1 x_2) ≫
        Iso.hom
            (isoMk (fun (X : Cᵒᵖ) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X) (x_2.obj X))
              sorry) ≫
          Iso.inv (α_ x_2 x x_1))
      X)
    (Hom.app
      (x ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x_2.obj X)) sorry) ≫
        Iso.inv (α_ x x_2 x_1) ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) sorry) ▷ x_1)
      X)
Tactic: ext : 1
-- 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))
⊢ CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x)
      (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯))
      (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x.obj X)) ⋯)) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
have h : ∀ (X : Cᵒᵖ),
  Hom.app
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x)
        (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) sorry))
        (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x.obj X)) sorry)))
      X =
    Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback (goal)
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (Functor.obj yoneda (F.obj X)) ⟶ M
| ((freeYonedaEquiv :
        (a : freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))).obj ((pushforward₀Obj F R N).obj (op X))) :
            Type u))
      (({ toFun := fun (g_1 : freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) ↦ g_1 ≫ (pushforward φ).map g } :
            (a : freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N)
          (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                  (freeObj (Functor.obj yoneda (F.obj X)) ⟶ M) ≃
                    (freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M)) :
                (a : freeObj (yoneda.obj (F.obj X)) ⟶ M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M)
              f :
            freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) :
        freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj N) :
    (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))) ((pushforward₀Obj F R N).obj (op X))) :
      Type u))
have erw : ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(S.obj (op X)) : Type u)) ↦
        LinearMap (R := (↑(S.obj (op X)) : Type u)) (RingHom.id (↑(S.obj (op X)) : Type u)) (↑x1 : Type u)
          (↑x2 : Type u))
        (CC := ModuleCat.carrier) (((pushforward φ).map g).app (op X)) :
      (a : (↑(((pushforward φ).obj M).obj (op X)) : Type u)) → (↑(((pushforward φ).obj N).obj (op X)) : Type u))
    ((freeYonedaEquiv :
          (a : (free S).obj (yoneda.obj X) ⟶ (pushforward φ).obj M) → (↑(((pushforward φ).obj M).obj (op X)) : Type u))
        (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                (freeObj (Functor.obj yoneda (F.obj X)) ⟶ M) ≃
                  (freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M)) :
              (a : freeObj (yoneda.obj (F.obj X)) ⟶ M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M)
            f :
          freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) :
      (↑(((pushforward φ).obj M).obj (op X)) : Type u)) :
  (↑(((pushforward φ).obj N).obj (op X)) : Type u))
Tactic: erw [freeYonedaEquiv_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback (goal)
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
⊢ pullbackObjIsDefined φ = ⊤
have h : ∀ (M : PresheafOfModules S), pullbackObjIsDefined φ M ↔ ⊤ M
Tactic: ext M
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback (goal)
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ pullbackObjIsDefined φ M ↔ ⊤ M
have h : pullbackObjIsDefined φ M
Tactic: simp only [Pi.top_apply, Prop.top_eq_true, iff_true]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback (goal)
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ pullbackObjIsDefined φ M
have h : ∀ (j : WalkingParallelPair), (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj j)
Tactic: apply leftAdjointObjIsDefined_of_isColimit
    M.isColimitFreeYonedaCoproductsCokernelCofork
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
M : PresheafOfModules.{u_1, v₂, u₂, u} R
X : Cᵒᵖ
⊢ M.map (F.op.map (𝟙 X)) =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
      (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))
have refine : ∀ (x : (↑(M.obj (F.op.obj X)) : Type u_1)),
  Eq (α :=
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
    ((ModuleCat.Hom.hom (M.map (F.op.map (𝟙 X))) :
          (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) :
              Type u_1))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
    ((ModuleCat.Hom.hom
            ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) sorry).inv.app
              (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))) :
          (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) :
              Type u_1))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
Tactic: refine ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
M : PresheafOfModules.{u_1, v₂, u₂, u} R
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat.{u_1, u} (↑((F.op ⋙ R).obj X) : Type u))
      (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))
      (Functor.obj (C := ModuleCat.{u_1, u} (↑((F.op ⋙ R).obj Z) : Type u))
        (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))))
        (ModuleCat.of (↑((F.op ⋙ R).obj Z) : Type u) (↑(M.obj (F.op.obj Z)) : Type u_1))))
    (M.map (F.op.map (f ≫ g)))
    (M.map (F.op.map f) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map f))).map (M.map (F.op.map g)) ≫
        NatTrans.app
          (Iso.inv
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((F.op ⋙ R).map f)) (RingCat.Hom.hom ((F.op ⋙ R).map g))
              (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))) ⋯))
          (ModuleCat.of (↑((F.op ⋙ R).obj Z) : Type u) (↑(M.obj (F.op.obj Z)) : Type u_1)))
have refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
T : CategoryTheory.Functor.{v₃, u, u₃, u + 1} Eᵒᵖ RingCat
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D E
ψ : R ⟶ G.op ⋙ T
T' : CategoryTheory.Functor.{v₄, u, u₄, u + 1} E'ᵒᵖ RingCat
G' : CategoryTheory.Functor.{v₃, v₄, u₃, u₄} E E'
ψ' : T ⟶ G'.op ⋙ T'
⊢ (pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (φ ≫ F.op.whiskerLeft ψ) ψ' =
    ((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫ pushforwardComp φ (ψ ≫ G.op.whiskerLeft ψ')
have w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
⊢ pushforwardComp (𝟙 S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor
have w : ∀ (x : PresheafOfModules.{v, v₂, u₂, u} R) (X : Cᵒᵖ)
  (x_1 : (↑(obj (Functor.obj (pushforward φ ⋙ pushforward (F := 𝟭 C) (𝟙 S)) x) X) : Type v)),
  Eq (α := (↑((Functor.obj (pushforward (F := 𝟭 C ⋙ F) (𝟙 S ≫ whiskerLeft (Functor.op (𝟭 C)) φ)) x).obj X) : Type v))
    ((ModuleCat.Hom.hom (Hom.app (NatTrans.app (Iso.hom (pushforwardComp (𝟙 S) φ)) x) X) :
          (a : (↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x).obj X) : Type v)) →
            (↑(((pushforward (𝟙 S ≫ (𝟭 C).op.whiskerLeft φ)).obj x).obj X) : Type v))
        x_1 :
      (↑((Functor.obj (pushforward (F := 𝟭 C ⋙ F) (𝟙 S ≫ whiskerLeft (Functor.op (𝟭 C)) φ)) x).obj X) : Type v))
    ((ModuleCat.Hom.hom
            ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x).app X) :
          (a : (↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x).obj X) : Type v)) →
            (↑(((pushforward (𝟙 S ≫ (𝟭 C).op.whiskerLeft φ)).obj x).obj X) : Type v))
        x_1 :
      (↑((Functor.obj (pushforward (F := 𝟭 C ⋙ F) (𝟙 S ≫ whiskerLeft (Functor.op (𝟭 C)) φ)) x).obj X) : Type v))
Tactic: ext