-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ 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)))
have erw : 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)))
      (HMul.hMul (α := S) (β := S)
        (((↑f.toMonoidWithZeroHom : ZeroHom R S) : (a : R) → S) ((RingHom.id R : (a : R) → R) r : R) : S) (1 : S)) :
    (↑X : Type (max u₂ u_1)))
Tactic: erw [smul_eq_mul]