awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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) φ
X : Cᵒᵖ
x : (↑(M₀.obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj ((sheafify α φ).val.obj X)) : Type v))
    ((ModuleCat.Hom.hom (Hom.app (toSheafify α φ) X) :
          (a : (↑(M₀.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj ((sheafify α φ).val.obj X)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj ((sheafify α φ).val.obj X)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₀.presheaf.obj X) : Type v)) → (↑(A.obj.obj X) : Type v))
        x :
      (↑(A.obj (P := Presheaf.IsSheaf J).obj X) : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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) φ
⊢ (toPresheaf R₀).map (toSheafify α φ) = φ

Tactic:
rfl

Premises used: AddMonoidHom.mk', rfl, PresheafOfModules.presheaf
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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) φ
dsimp :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
⊢ IsLocallyInjective J (M₂ := (restrictScalars α).obj (sheafify α φ).val) (toSheafify α φ)

Tactic:
dsimp [IsLocallyInjective]

Premises used: PresheafOfModules.IsLocallyInjective
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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) φ
⊢ Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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) φ
dsimp :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ
⊢ IsLocallySurjective J (M₂ := (restrictScalars α).obj (sheafify α φ).val) (toSheafify α φ)

Tactic:
dsimp [IsLocallySurjective]

Premises used: PresheafOfModules.IsLocallySurjective
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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) φ
⊢ Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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)
F : PresheafOfModules.{v, v₁, u₁, u} (R.obj (P := Presheaf.IsSheaf J))
hF : Presheaf.IsSheaf J F.presheaf
f : M₀ ⟶ (restrictScalars α).obj F
⊢ φ ≫
      (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
        ((Equiv.symm (sheafifyHomEquiv' α φ hF) : (a : M₀ ⟶ (restrictScalars α).obj F) → (sheafify α φ).val ⟶ F) f) =
    (toPresheaf R₀).map f

Tactic:
(toPresheaf _).congr_map ((sheafifyHomEquiv' α φ hF).apply_symm_apply f)

Premises used: CategoryTheory.NatTrans.vcomp, Equiv.apply_symm_apply, PresheafOfModules.restrictScalarsObj, PresheafOfModules.toPresheaf, CategoryTheory.Functor.congr_map, PresheafOfModules.sheafifyHomEquiv', PresheafOfModules.presheaf
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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)
⊢ Presheaf.IsSheaf J (sheafify α φ').val.presheaf

Tactic:
A'.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, AddMonoidHom.mk', PresheafOfModules.presheaf
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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)
⊢ Presheaf.IsSheaf J (sheafify α φ').val.presheaf

Tactic:
exact A'.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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 α φ')
this : τ.hom = (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map f
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (τ.hom.app X) :
        (a : (↑((sheafify α φ).val.presheaf.obj X) : Type v)) → (↑((sheafify α φ').val.presheaf.obj X) : Type v))
      (r • m) =
    HSMul.hSMul (β := (↑((sheafify α φ').val.presheaf.obj X) : Type v)) r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (τ.hom.app X) :
            (a : (↑((sheafify α φ).val.presheaf.obj X) : Type v)) → (↑((sheafify α φ').val.presheaf.obj X) : Type v))
          m :
        (↑((sheafify α φ').val.presheaf.obj X) : Type v))

Tactic:
simpa only [this] using (f.app X).hom.map_smul r m

Premises used: LinearMap.map_smul, ModuleCat.Hom.hom, PresheafOfModules.Hom.app
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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 α φ')
suffices : τ.hom = (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map f
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (τ.hom.app X) :
        (a : (↑((sheafify α φ).val.presheaf.obj X) : Type v)) → (↑((sheafify α φ').val.presheaf.obj X) : Type v))
      (r • m) =
    HSMul.hSMul (β := (↑((sheafify α φ').val.presheaf.obj X) : Type v)) r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (τ.hom.app X) :
            (a : (↑((sheafify α φ).val.presheaf.obj X) : Type v)) → (↑((sheafify α φ').val.presheaf.obj X) : Type v))
          m :
        (↑((sheafify α φ').val.presheaf.obj X) : Type v))

Tactic:
suffices τ.hom = (toPresheaf _).map f by simpa only [this] using (f.app X).hom.map_smul r m
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
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 :
  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))
⊢ τ.hom = (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map f

Tactic:
apply ((J.W_of_isLocallyBijective φ).homEquiv _ A'.property).injective

Premises used: CategoryTheory.GrothendieckTopology.W_of_isLocallyBijective, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.isLocal.homEquiv, Equiv.injective