-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R₀ R : Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
α : R₀ ⟶ R
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst_2 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
hA :
  Presheaf.IsSeparated J A (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier)
Y : C
r₀ r₀' : (↑(R₀.obj (Opposite.op Y)) : Type u)
m₀ m₀' : (↑(M₀.obj (Opposite.op Y)) : Type v)
hr₀ :
  Eq (α := (↑(R.obj (Opposite.op Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Y)) (α.app (Opposite.op Y)) :
          (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R.obj (Opposite.op Y)) : Type u))
        r₀ :
      (↑(R.obj (Opposite.op Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Y)) (α.app (Opposite.op Y)) :
          (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R.obj (Opposite.op Y)) : Type u))
        r₀' :
      (↑(R.obj (Opposite.op Y)) : Type u))
hm₀ :
  Eq (α := (↑(A.obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj (Opposite.op Y)) : Type v))
        m₀ :
      (↑(A.obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj (Opposite.op Y)) : Type v))
        m₀' :
      (↑(A.obj (Opposite.op Y)) : Type v))
Z : C
g : Z ⟶ Opposite.unop (Opposite.op Y)
hg :
  (Presheaf.equalizerSieve (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier) r₀
          r₀' ⊓
        Presheaf.equalizerSieve (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
          AddCommGrpCat.carrier) (F := M₀.presheaf) m₀ m₀').arrows
    g
a :
  Eq (α := (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        (HSMul.hSMul (α := (↑(R₀.obj (Opposite.op Z)) : Type u)) (β :=
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.obj (Opposite.op Z))) : Type v))
          ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  RingCat.carrier) (R₀.map g.op) :
                (a : (↑(R₀.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type u)) →
                  (↑(R₀.obj (Opposite.op Z)) : Type u))
              r₀' :
            (↑(R₀.obj (Opposite.op Z)) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                  AddCommGrpCat.carrier) (M₀.presheaf.map g.op) :
                (a : (↑(M₀.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) →
                  (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))
              m₀' :
            (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))) :
      (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        (HSMul.hSMul (α := (↑(R₀.obj (Opposite.op Z)) : Type u)) (β :=
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.obj (Opposite.op Z))) : Type v))
          ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  RingCat.carrier) (R₀.map g.op) :
                (a : (↑(R₀.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type u)) →
                  (↑(R₀.obj (Opposite.op Z)) : Type u))
              r₀' :
            (↑(R₀.obj (Opposite.op Z)) : Type u))
          ((ConcreteCategory.hom (FC :=
                  fun (x1 x2 : ModuleCat.{v, u} (↑(R₀.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R₀.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type u))
                    (RingHom.id (↑(R₀.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (M₀.map g.op) :
                (a : (↑(M₀.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.obj (Opposite.op Z))) :
                    Type v))
              m₀' :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.obj (Opposite.op Z))) : Type v))) :
      (↑(A.obj (Opposite.op Z)) : Type v))
⊢ Eq (α := (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M₀.presheaf.map g.op) :
              (a : (↑(M₀.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) →
                (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))
            (r₀ • m₀) :
          (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) :
      (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M₀.presheaf.map g.op) :
              (a : (↑(M₀.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) →
                (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))
            (r₀' • m₀') :
          (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) :
      (↑(A.obj (Opposite.op Z)) : Type v))

Tactic:
erw [M₀.map_smul, M₀.map_smul, hg.1, hg.2]

Premises used: PresheafOfModules.map_smul, And.right, And.left