-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules.{v, v', u', u} R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst_1 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : (↑(R'.obj X) : Type u)
m : (↑(M₁.obj X) : Type v)
Y : C
p : Y ⟶ Opposite.unop X
r : (↑(R.obj (Opposite.op Y)) : Type u)
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)
            (R'.map p.op) :
          (a : (↑(R'.obj (Opposite.op (Opposite.unop X))) : Type u)) → (↑(R'.obj (Opposite.op Y)) : Type u))
        r' :
      (↑(R'.obj (Opposite.op Y)) : Type u))
hg :
  ∀ (z : (↑(M₁.obj X) : Type v)),
    Eq (α :=
      (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))) (M₂.obj (Opposite.op Y))) :
        Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op Y)) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op Y)) : Type u))
                (RingHom.id (↑(R.obj (Opposite.op Y)) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
              (CC := ModuleCat.carrier) (g.app (Opposite.op Y)) :
            (a :
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₁.obj (Opposite.op Y))) :
                  Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₂.obj (Opposite.op Y))) :
                Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u))
                    (↑x1 : Type v) (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (M₁.map p.op) :
                (a : (↑(M₁.obj X) : Type v)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) :
                    Type v))
              z :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) : Type v)) :
        (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))) (M₂.obj (Opposite.op Y))) :
          Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M₂.map p.op) :
            (a : (↑(M₂.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (g.app X) :
                (a : (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M₁.obj X)) : Type v)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M₂.obj X)) : Type v))
              z :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M₂.obj X)) : Type v)) :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v))
a :
  Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op Y)) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op Y)) : Type u))
              (RingHom.id (↑(R.obj (Opposite.op Y)) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (g.app (Opposite.op Y)) :
          (a :
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₁.obj (Opposite.op Y))) :
                Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₂.obj (Opposite.op Y))) :
              Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M₁.map p.op) :
              (a : (↑(M₁.obj X) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) : Type v))
            (r' • m) :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) : Type v)) :
      (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))) (M₂.obj (Opposite.op Y))) :
        Type v))
    ((ModuleCat.Hom.hom (g.app (Opposite.op Y)) :
          (a : (↑(((restrictScalars α).obj M₁).obj (Opposite.op Y)) : Type v)) →
            (↑(((restrictScalars α).obj M₂).obj (Opposite.op Y)) : Type v))
        (HSMul.hSMul (β := (↑(((restrictScalars α).obj M₁).obj (Opposite.op Y)) : Type v)) r
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u))
                    (↑x1 : Type v) (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (M₁.map p.op) :
                (a : (↑(M₁.obj X) : Type v)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) :
                    Type v))
              m :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) : Type v))) :
      (↑(((restrictScalars α).obj M₂).obj (Opposite.op Y)) : Type v))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op Y)) : Type u)) ↦
          LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op Y)) : Type u))
            (RingHom.id (↑(R.obj (Opposite.op Y)) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
          (CC := ModuleCat.carrier) (g.app (Opposite.op Y)) :
        (a :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₁.obj (Opposite.op Y))) :
              Type v)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₂.obj (Opposite.op Y))) :
            Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M₁.map p.op) :
            (a : (↑(M₁.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) : Type v))
          (r' • m) :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) : Type v)) =
    HSMul.hSMul (α := (↑(R'.obj (Opposite.op Y)) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v))
      ((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 (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op Y)) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op Y)) : Type u))
                (RingHom.id (↑(R.obj (Opposite.op Y)) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
              (CC := ModuleCat.carrier) (g.app (Opposite.op Y)) :
            (a :
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₁.obj (Opposite.op Y))) :
                  Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))).obj (M₂.obj (Opposite.op Y))) :
                Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u))
                    (↑x1 : Type v) (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (M₁.map p.op) :
                (a : (↑(M₁.obj X) : Type v)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) :
                    Type v))
              m :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map p.op))).obj (M₁.obj (Opposite.op Y))) : Type v)) :
        (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app (Opposite.op Y)))) (M₂.obj (Opposite.op Y))) :
          Type v))

Tactic:
erw [← (g.app _).hom.map_smul]

Premises used: LinearMap.map_smul, ModuleCat.Hom.hom, PresheafOfModules.Hom.app