awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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)))

Tactic:
ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))

Premises used: LinearMap.ext, ModuleCat.hom_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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)))

Tactic:
refine ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))

Premises used: LinearMap.ext, ModuleCat.hom_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
x : (↑(M.obj (F.op.obj X)) : Type u_1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
x : (↑(M.obj (F.op.obj X)) : Type u_1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (M.congr_map_apply (F.op.map_comp f g) x).trans (by simp)

Premises used: CategoryTheory.Functor.op, PresheafOfModules.congr_map_apply, CategoryTheory.Functor.map_comp, Eq.trans
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
M : PresheafOfModules.{v, v₂, u₂, u} R
X Y : Cᵒᵖ
f : X ⟶ Y
m :
  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X))))) :
    Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.map f))).obj (((pushforward φ).obj M).obj Y)) : Type v))
    ((ModuleCat.Hom.hom (((pushforward φ).obj M).map f) :
          (a : (↑(((pushforward φ).obj M).obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.map f))).obj (((pushforward φ).obj M).obj Y)) : Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.map f))).obj (((pushforward φ).obj M).obj Y)) : Type v))
    ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u))
              (RingHom.id (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map (F.map f.unop).op) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.map f.unop).op))).obj
                  (M.obj (Opposite.op (F.obj (Opposite.unop Y))))) :
              Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.map f.unop).op))).obj
            (M.obj (Opposite.op (F.obj (Opposite.unop Y))))) :
        Type v))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
M : PresheafOfModules.{v, v₂, u₂, u} R
X Y : Cᵒᵖ
f : X ⟶ Y
m :
  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X))))) :
    Type v)
⊢ Eq (α :=
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.map f))).obj
          ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app Y))).obj (((pushforward₀ F R).obj M).obj Y))) :
      Type v))
    ((ModuleCat.Hom.hom (((pushforward φ).obj M).map f) :
          (a :
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj
                    (M.obj (Opposite.op (F.obj (Opposite.unop X))))) :
                Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.map f))).obj
                  ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app Y))).obj (((pushforward₀ F R).obj M).obj Y))) :
              Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.map f))).obj
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app Y))).obj (((pushforward₀ F R).obj M).obj Y))) :
        Type v))
    ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u))
              (RingHom.id (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map (F.map f.unop).op) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.map f.unop).op))).obj
                  (M.obj (Opposite.op (F.obj (Opposite.unop Y))))) :
              Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.map f.unop).op))).obj
            (M.obj (Opposite.op (F.obj (Opposite.unop Y))))) :
        Type v))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
M N : PresheafOfModules.{v, v₂, u₂, u} R
α : M ⟶ N
X : Cᵒᵖ
m :
  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X))))) :
    Type v)
⊢ Eq (α := (↑(((pushforward φ).obj N).obj X) : Type v))
    ((ModuleCat.Hom.hom (((pushforward φ).map α).app X) :
          (a : (↑(((pushforward φ).obj M).obj X) : Type v)) → (↑(((pushforward φ).obj N).obj X) : Type v))
        m :
      (↑(((pushforward φ).obj N).obj X) : Type v))
    ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u))
              (RingHom.id (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (α.app (Opposite.op (F.obj (Opposite.unop X)))) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
        m :
      (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
M N : PresheafOfModules.{v, v₂, u₂, u} R
α : M ⟶ N
X : Cᵒᵖ
m :
  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X))))) :
    Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (((pushforward₀ F R).obj N).obj X)) : Type v))
    ((ModuleCat.Hom.hom (((pushforward φ).map α).app X) :
          (a :
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj
                    (M.obj (Opposite.op (F.obj (Opposite.unop X))))) :
                Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (((pushforward₀ F R).obj N).obj X)) :
              Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (((pushforward₀ F R).obj N).obj X)) : Type v))
    ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u))
              (RingHom.id (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (α.app (Opposite.op (F.obj (Opposite.unop X)))) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
        m :
      (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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'
w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (φ ≫ F.op.whiskerLeft ψ) ψ' =
    ((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫ pushforwardComp φ (ψ ≫ G.op.whiskerLeft ψ')

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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'
x : PresheafOfModules.{u_1, v₄, u₄, u} T'
X : Cᵒᵖ
x_1 : (↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x).obj X) : Type u_1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
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))
⊢ pushforwardComp (𝟙 S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
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:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
w :
  ∀ (x : PresheafOfModules.{v, v₂, u₂, u} R) (X : Cᵒᵖ)
    (x_1 : (↑((Functor.obj (pushforward (F := 𝟭 D) (𝟙 R) ⋙ pushforward φ) x).obj X) : Type v)),
    Eq (α := (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
      ((ModuleCat.Hom.hom (Hom.app (NatTrans.app (Iso.hom (pushforwardComp φ (𝟙 R))) x) X) :
            (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).obj X) : Type v)) →
              (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
          x_1 :
        (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
      ((ModuleCat.Hom.hom
              (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x).app X) :
            (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).obj X) : Type v)) →
              (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
          x_1 :
        (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
⊢ pushforwardComp φ (𝟙 R) = isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
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
x : PresheafOfModules.{v, v₂, u₂, u} R
X : Cᵒᵖ
x_1 : (↑((Functor.obj (pushforward (F := 𝟭 D) (𝟙 R) ⋙ pushforward φ) x).obj X) : Type v)
⊢ Eq (α := (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
    ((ModuleCat.Hom.hom (Hom.app (NatTrans.app (Iso.hom (pushforwardComp φ (𝟙 R))) x) X) :
          (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).obj X) : Type v)) →
            (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
        x_1 :
      (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
    ((ModuleCat.Hom.hom
            (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x).app X) :
          (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).obj X) : Type v)) →
            (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
        x_1 :
      (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R₀ : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj (P := Presheaf.IsSheaf J)
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
inst_2 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
⊢ (SheafOfModules.toSheaf R).ReflectsIsomorphisms

Tactic:
have : (SheafOfModules.toSheaf.{v} R ⋙ sheafToPresheaf _ _).ReflectsIsomorphisms :=
    inferInstanceAs (SheafOfModules.forget.{v} R ⋙ toPresheaf _).ReflectsIsomorphisms
  reflectsIsomorphisms_of_comp _ (sheafToPresheaf _ _)

Premises used: _private.0.PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf._proof_1, SheafOfModules.toSheaf, AddCommGrpCat, CategoryTheory.sheafToPresheaf, CategoryTheory.reflectsIsomorphisms_of_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R₀ : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj (P := Presheaf.IsSheaf J)
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
inst_2 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_4 : HasWeakSheafify J AddCommGrpCat
X Y : PresheafOfModules.{v, v', u', u} R₀
f : X ⟶ Y
⊢ (toPresheaf R₀).map f ≫ CategoryTheory.toSheafify J Y.presheaf =
    CategoryTheory.toSheafify J X.presheaf ≫ ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map f).hom

Tactic:
apply toSheafify_naturality

Premises used: CategoryTheory.toSheafify_naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R₀ : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj (P := Presheaf.IsSheaf J)
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
inst_2 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_4 : HasWeakSheafify J AddCommGrpCat
M₀ : PresheafOfModules.{v, v', u', u} R₀
h :
  SheafOfModules.Hom.val
      (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯) =
    SheafOfModules.Hom.val
      (𝟙 (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf)))
⊢ sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
      ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯ =
    𝟙 (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf))

Tactic:
ext1