-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
protected lemma smul_zero : smul α φ r 0 = 0

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.val.obj X)
⊢ smul α φ r 0 = 0

Tactic:
apply A.isSeparated _ _ (Presheaf.imageSieve_mem J α r)

Result:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.val.obj X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    (Presheaf.imageSieve α r).arrows f →
      (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r 0) = (ConcreteCategory.hom (A.val.map f.op)) 0

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.val.obj X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.val.map f.op)) r
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) 0 = (ConcreteCategory.hom (A.val.map f.op)) 0

Tactic:
simp

Result:
no goals

Proof state:
case a.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.val.obj X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.val.map f.op)) r
⊢ (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r 0) = (ConcreteCategory.hom (A.val.map f.op)) 0

Tactic:
rw [(A.val.map f.op).hom.map_zero, map_smul_eq α φ r 0 f.op r₀ hr₀ 0 (by simp),
  smul_zero, map_zero]

Result:
no goals

Proof state:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.val.obj X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    (Presheaf.imageSieve α r).arrows f →
      (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r 0) = (ConcreteCategory.hom (A.val.map f.op)) 0

Tactic:
rintro Y f ⟨r₀, hr₀⟩

Result:
case a.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.val.obj X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.val.map f.op)) r
⊢ (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r 0) = (ConcreteCategory.hom (A.val.map f.op)) 0