awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify (goal)
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) α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj (P := Presheaf.IsSheaf J)
inst_3 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
inst_4 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ
inst_5 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
M₀' : PresheafOfModules.{v, v₁, u₁, u} R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J)
inst_6 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ'
inst_7 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)
m : (↑((sheafify α φ).val.obj X) : Type v)
f : (sheafify α φ).val ⟶ (sheafify α φ').val :=
  (Equiv.symm (sheafifyHomEquiv' α φ ⋯) :
      (a : M₀ ⟶ (restrictScalars α).obj (sheafify α φ').val) → (sheafify α φ).val ⟶ (sheafify α φ').val)
    (τ₀ ≫ toSheafify α φ')
⊢ Eq (α := M₀.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J))
    ((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ (A'.obj (P := Presheaf.IsSheaf J)) ⋯ :
          (a : A.obj ⟶ A'.obj) → M₀.presheaf ⟶ A'.obj)
        τ.hom :
      M₀.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J))
    ((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ (A'.obj (P := Presheaf.IsSheaf J)) ⋯ :
          (a : A.obj ⟶ A'.obj) → M₀.presheaf ⟶ A'.obj)
        ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map f) :
      M₀.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J))
have a : φ ≫ τ.hom =
  φ ≫
    (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      ((Equiv.symm (sheafifyHomEquiv' α φ sorry) :
          (a : M₀ ⟶ (sheafify α φ').val.restrictScalarsObj α) → (sheafify α φ).val ⟶ (sheafify α φ').val)
        (τ₀ ≫ toSheafify α φ'))
Tactic: dsimp [f]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify (goal)
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) α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj (P := Presheaf.IsSheaf J)
inst_3 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
inst_4 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ
inst_5 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
M₀' : PresheafOfModules.{v, v₁, u₁, u} R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J)
inst_6 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ'
inst_7 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)
m : (↑((sheafify α φ).val.obj X) : Type v)
f : (sheafify α φ).val ⟶ (sheafify α φ').val :=
  (Equiv.symm (sheafifyHomEquiv' α φ ⋯) :
      (a : M₀ ⟶ (restrictScalars α).obj (sheafify α φ').val) → (sheafify α φ).val ⟶ (sheafify α φ').val)
    (τ₀ ≫ toSheafify α φ')
⊢ φ ≫ τ.hom =
    φ ≫
      (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
        ((Equiv.symm (sheafifyHomEquiv' α φ ⋯) :
            (a : M₀ ⟶ (sheafify α φ').val.restrictScalarsObj α) → (sheafify α φ).val ⟶ (sheafify α φ').val)
          (τ₀ ≫ toSheafify α φ'))
have a : φ ≫ τ.hom = (toPresheaf R₀).map (τ₀ ≫ toSheafify α φ')
Tactic: erw [comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify (goal)
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) α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj (P := Presheaf.IsSheaf J)
inst_3 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
inst_4 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ
inst_5 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
M₀' : PresheafOfModules.{v, v₁, u₁, u} R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J)
inst_6 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ'
inst_7 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)
m : (↑((sheafify α φ).val.obj X) : Type v)
f : (sheafify α φ).val ⟶ (sheafify α φ').val :=
  (Equiv.symm (sheafifyHomEquiv' α φ ⋯) :
      (a : M₀ ⟶ (restrictScalars α).obj (sheafify α φ').val) → (sheafify α φ).val ⟶ (sheafify α φ').val)
    (τ₀ ≫ toSheafify α φ')
⊢ φ ≫ τ.hom = (toPresheaf R₀).map (τ₀ ≫ toSheafify α φ')
have a : (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map (τ₀ ≫ toSheafify α φ')
Tactic: rw [← fac, Functor.map_comp, toPresheaf_map_toSheafify]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify (goal)
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) α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj (P := Presheaf.IsSheaf J)
inst_3 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
inst_4 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ
inst_5 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
M₀' : PresheafOfModules.{v, v₁, u₁, u} R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J)
inst_6 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ'
inst_7 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)
m : (↑((sheafify α φ).val.obj X) : Type v)
f : (sheafify α φ).val ⟶ (sheafify α φ').val :=
  (Equiv.symm (sheafifyHomEquiv' α φ ⋯) :
      (a : M₀ ⟶ (restrictScalars α).obj (sheafify α φ').val) → (sheafify α φ).val ⟶ (sheafify α φ').val)
    (τ₀ ≫ toSheafify α φ')
a : (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map (τ₀ ≫ toSheafify α φ')
⊢ φ ≫ τ.hom = (toPresheaf R₀).map (τ₀ ≫ toSheafify α φ')
have a₁ : (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map τ₀ ≫ (toPresheaf R₀).map (toSheafify α φ')
Tactic: rw [← fac, Functor.map_comp, toPresheaf_map_toSheafify]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify (goal)
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) α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj (P := Presheaf.IsSheaf J)
inst_3 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
inst_4 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ
inst_5 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
M₀' : PresheafOfModules.{v, v₁, u₁, u} R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj (P := Presheaf.IsSheaf J)
inst_6 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ'
inst_7 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)
m : (↑((sheafify α φ).val.obj X) : Type v)
f : (sheafify α φ).val ⟶ (sheafify α φ').val :=
  (Equiv.symm (sheafifyHomEquiv' α φ ⋯) :
      (a : M₀ ⟶ (restrictScalars α).obj (sheafify α φ').val) → (sheafify α φ).val ⟶ (sheafify α φ').val)
    (τ₀ ≫ toSheafify α φ')
a : (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map (τ₀ ≫ toSheafify α φ')
a₁ : (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map τ₀ ≫ (toPresheaf R₀).map (toSheafify α φ')
⊢ φ ≫ τ.hom = (toPresheaf R₀).map (τ₀ ≫ toSheafify α φ')
have a₂ : (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map τ₀ ≫ φ'
Tactic: rw [← fac, Functor.map_comp, toPresheaf_map_toSheafify]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M : PresheafOfModules.{v, v₁, u₁, u} R
X Y : Cᵒᵖ
f g : X ⟶ Y
h : f = g
m : (↑(M.obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map g) :
          (a : (↑(M.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
have rw : Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
          LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
            (↑x2 : Type v))
          (CC := ModuleCat.carrier) (M.map g) :
        (a : (↑(M.obj X) : Type v)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
      m :
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
          LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
            (↑x2 : Type v))
          (CC := ModuleCat.carrier) (M.map g) :
        (a : (↑(M.obj X) : Type v)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
      m :
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ X_1 Y_1 : PresheafOfModules.{v, v₁, u₁, u} R
f : X_1 ⟶ Y_1
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ X_1.presheaf.map g ≫
      AddCommGrpCat.ofHom
        (AddMonoidHom.mk'
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app Y)) :
            (a : (↑(X_1.obj Y) : Type v)) → (↑(Y_1.obj Y) : Type v))
          ⋯) =
    AddCommGrpCat.ofHom
        (AddMonoidHom.mk'
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app X)) :
            (a : (↑(X_1.obj X) : Type v)) → (↑(Y_1.obj X) : Type v))
          ⋯) ≫
      Y_1.presheaf.map g
have hf : ∀ (x : (↑(X_1.presheaf.obj X) : Type v)),
  Eq (α := (↑(Y_1.presheaf.obj Y) : Type v))
    ((AddCommGrpCat.Hom.hom
            (X_1.presheaf.map g ≫
              AddCommGrpCat.ofHom
                (AddMonoidHom.mk'
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                        LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u))
                          (↑x1 : Type v) (↑x2 : Type v))
                        (CC := ModuleCat.carrier) (f.app Y)) :
                    (a : (↑(X_1.obj Y) : Type v)) → (↑(Y_1.obj Y) : Type v))
                  sorry)) :
          (a : (↑(X_1.presheaf.obj X) : Type v)) → (↑(Y_1.presheaf.obj Y) : Type v))
        x :
      (↑(Y_1.presheaf.obj Y) : Type v))
    ((AddCommGrpCat.Hom.hom
            (AddCommGrpCat.ofHom
                (AddMonoidHom.mk'
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                        LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u))
                          (↑x1 : Type v) (↑x2 : Type v))
                        (CC := ModuleCat.carrier) (f.app X)) :
                    (a : (↑(X_1.obj X) : Type v)) → (↑(Y_1.obj X) : Type v))
                  sorry) ≫
              Y_1.presheaf.map g) :
          (a : (↑(X_1.presheaf.obj X) : Type v)) → (↑(Y_1.presheaf.obj Y) : Type v))
        x :
      (↑(Y_1.presheaf.obj Y) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
x x_1 : PresheafOfModules.{u_1, v₁, u₁, u} R
f g : x ⟶ x_1
h : (toPresheaf R).map f = (toPresheaf R).map g
⊢ f = g
have h₁ : ∀ (X : Cᵒᵖ) (x_2 : (↑(x.obj X) : Type u_1)),
  Eq (α := (↑(x_1.obj X) : Type u_1))
    ((ModuleCat.Hom.hom (f.app X) : (a : (↑(x.obj X) : Type u_1)) → (↑(x_1.obj X) : Type u_1)) x_2 :
      (↑(x_1.obj X) : Type u_1))
    ((ModuleCat.Hom.hom (g.app X) : (a : (↑(x.obj X) : Type u_1)) → (↑(x_1.obj X) : Type u_1)) x_2 :
      (↑(x_1.obj X) : Type u_1))
Tactic: ext X x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (-f.app Y) = (-f.app X) ≫ M₂.map h
have hf : ∀ (x : (↑(M₁.obj X) : Type v)),
  Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom (M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (-f.app Y)) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom ((-f.app X) ≫ M₂.map h) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y) =
    (f.app X + g.app X) ≫ M₂.map h
have hf : ∀ (x : (↑(M₁.obj X) : Type v)),
  Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom (M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y)) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom ((f.app X + g.app X) ≫ M₂.map h) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y - g.app Y) =
    (f.app X - g.app X) ≫ M₂.map h
have hf : ∀ (x : (↑(M₁.obj X) : Type v)),
  Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom (M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y - g.app Y)) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom ((f.app X - g.app X) ≫ M₂.map h) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
a b c : M₁ ⟶ M₂
⊢ a + b + c = a + (b + c)
have h : ∀ (X : Cᵒᵖ), (a + b + c).app X = (a + (b + c)).app X
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
a : M₁ ⟶ M₂
⊢ 0 + a = a
have h : ∀ (X : Cᵒᵖ), (0 + a).app X = a.app X
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
a : M₁ ⟶ M₂
⊢ a + 0 = a
have h : ∀ (X : Cᵒᵖ), (a + 0).app X = a.app X
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
a b : M₁ ⟶ M₂
⊢ a - b = a + -b
have h : ∀ (X : Cᵒᵖ), (a - b).app X = (a + -b).app X
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
a : M₁ ⟶ M₂
⊢ -a + a = 0
have h : ∀ (X : Cᵒᵖ), (-a + a).app X = Hom.app 0 X
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
a b : M₁ ⟶ M₂
⊢ a + b = b + a
have h : ∀ (X : Cᵒᵖ), (a + b).app X = (b + a).app X
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (n • f).app X = n • f.app X
have hf : ∀ (x : (↑(M₁.obj X) : Type v)),
  Eq (α := (↑(M₂.obj X) : Type v))
    ((ModuleCat.Hom.hom ((n • f).app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
Tactic: ext x