-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
lemma isCompatible_map_smul : ((r₀.smul m₀).map (whiskerRight φ (forget _))).Compatible

Proof state:
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ᵒᵖ ⥤ AddCommGrp
φ : 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
⊢ (A ⋙ forget Ab).map g₁.op ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
    (A ⋙ forget Ab).map g₂.op ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)

Tactic:
have ha₀ : (α.app (Opposite.op Z)) a₀ = (R.map (f₁.op ≫ g₁.op)) r := by
  dsimp [a₀]
  rw [← RingCat.comp_apply, NatTrans.naturality, RingCat.comp_apply, ha₁, Functor.map_comp,
    RingCat.comp_apply]

Result:
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ᵒᵖ ⥤ AddCommGrp
φ : 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
⊢ (A ⋙ forget Ab).map g₁.op ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
    (A ⋙ forget Ab).map g₂.op ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)

Proof state:
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ᵒᵖ ⥤ AddCommGrp
φ : 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
⊢ (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₂.op ≫ g₂.op))) r

Tactic:
rw [ha₀, ← op_comp, fac, op_comp]

Result:
no goals