-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
r : R
y : (↑Y : Type (max u₂ u_1))
rw :
  Eq (α := (↑X : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f X :
                (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                    (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                  (a : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                (r • y)) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
        1 :
      (↑X : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f X :
                (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                    (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                  (a : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                y) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
        (HSMul.hSMul (α := R) (β := (↑((restrictScalars f).obj (of S S)) : Type u₂))
          ((RingHom.id R : (a : R) → R) r : R) 1) :
      (↑X : Type (max u₂ u_1)))
⊢ (((CoextendScalars.equiv f X :
              (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                  (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                (a : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
              (r • y)) :
          (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
      1 =
    HSMul.hSMul (α := R) (β := (↑X : Type (max u₂ u_1))) ((RingHom.id R : (a : R) → R) r : R)
      ((((CoextendScalars.equiv f X :
                (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                    (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                  (a : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                y) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
        1)

Tactic:
rw [← map_smul]

Premises used: map_smul