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))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
a₀ : ↑(R₀.obj (Opposite.op Z)) := (ConcreteCategory.hom (R₀.map g₁.op)) a₁
b₀ : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) :=
  (ConcreteCategory.hom (M₀.map g₁.op)) b₁
ha₁ : (ConcreteCategory.hom (α.app (Opposite.op Y₁))) a₁ = (ConcreteCategory.hom (R.map f₁.op)) r
ha₂ : (ConcreteCategory.hom (α.app (Opposite.op Y₂))) a₂ = (ConcreteCategory.hom (R.map f₂.op)) r
hb₁ : (ConcreteCategory.hom (φ.app (Opposite.op Y₁))) b₁ = (ConcreteCategory.hom (A.map f₁.op)) m
hb₂ : (ConcreteCategory.hom (φ.app (Opposite.op Y₂))) b₂ = (ConcreteCategory.hom (A.map f₂.op)) m
ha₀ : (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₁.op ≫ g₁.op))) r
hb₀ : (ConcreteCategory.hom (φ.app (Opposite.op Z))) b₀ = (ConcreteCategory.hom (A.map (f₁.op ≫ g₁.op))) m
ha₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₂.op ≫ g₂.op))) r
hb₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) b₀ = (ConcreteCategory.hom (A.map (f₂.op ≫ g₂.op))) m
⊢ (ConcreteCategory.hom (A.map g₁.op))
      ({ toFun := ⇑(ConcreteCategory.hom (φ.app (Opposite.op Y₁))) } (r₀.smul m₀ f₁ h₁)) =
    (ConcreteCategory.hom (A.map g₂.op))
      ({ toFun := ⇑(ConcreteCategory.hom (φ.app (Opposite.op Y₂))) } (r₀.smul m₀ f₂ h₂))

Tactic:
erw [← NatTrans.naturality_apply φ, ← NatTrans.naturality_apply φ]

Goal state after:
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))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
a₀ : ↑(R₀.obj (Opposite.op Z)) := (ConcreteCategory.hom (R₀.map g₁.op)) a₁
b₀ : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) :=
  (ConcreteCategory.hom (M₀.map g₁.op)) b₁
ha₁ : (ConcreteCategory.hom (α.app (Opposite.op Y₁))) a₁ = (ConcreteCategory.hom (R.map f₁.op)) r
ha₂ : (ConcreteCategory.hom (α.app (Opposite.op Y₂))) a₂ = (ConcreteCategory.hom (R.map f₂.op)) r
hb₁ : (ConcreteCategory.hom (φ.app (Opposite.op Y₁))) b₁ = (ConcreteCategory.hom (A.map f₁.op)) m
hb₂ : (ConcreteCategory.hom (φ.app (Opposite.op Y₂))) b₂ = (ConcreteCategory.hom (A.map f₂.op)) m
ha₀ : (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₁.op ≫ g₁.op))) r
hb₀ : (ConcreteCategory.hom (φ.app (Opposite.op Z))) b₀ = (ConcreteCategory.hom (A.map (f₁.op ≫ g₁.op))) m
ha₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₂.op ≫ g₂.op))) r
hb₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) b₀ = (ConcreteCategory.hom (A.map (f₂.op ≫ g₂.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.presheaf.map g₁.op)) (r₀.smul m₀ f₁ h₁)) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.presheaf.map g₂.op)) (r₀.smul m₀ f₂ h₂))