Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) (r₀ • m₀)) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) (r₀' • m₀')

Tactic:
rw [← PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective α φ hA (R₀.map g.op r₀) r₀'
    (M₀.map g.op m₀) m₀', M₀.map_smul]

Goal state after:
case hr₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Z))) ((ConcreteCategory.hom (R₀.map g.op)) r₀) =
    (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀'

case hm₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀'