-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_7
S : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_9
inst_3 : CommSemiring A
inst_4 : Algebra R A
M : Submonoid R
inst_5 : IsLocalization M A
s : S
x : R
y : ↥M
rw :
  HMul.hMul (α := S ⊗[R] A) (β := S ⊗[R] A) (s ⊗ₜ[R] mk' A x y)
      ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A)
          (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                ((algebraMap R S : (a : R) → S) (↑y : R)) ⋯) :
            S) :
        S ⊗[R] A) =
    (algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s)
rw₁ :
  HMul.hMul (α := S ⊗[R] A) (β := S ⊗[R] A) (s ⊗ₜ[R] mk' A x y)
      ((algebraMap S S : (a : S) → S)
            ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    ((algebraMap R S : (a : R) → S) (↑y : R)) ⋯) :
                S) :
              S) ⊗ₜ[R]
          1 :
        S ⊗[R] A) =
    (algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s)
rw₂ :
  HMul.hMul (α := S ⊗[R] A) (β := S ⊗[R] A) (s ⊗ₜ[R] mk' A x y)
      ((RingHom.id S : (a : S) → S)
            ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    ((algebraMap R S : (a : R) → S) (↑y : R)) ⋯) :
                S) :
              S) ⊗ₜ[R]
          1 :
        S ⊗[R] A) =
    (algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s)
rw₃ :
  HMul.hMul (α := S ⊗[R] A) (β := S ⊗[R] A) (s ⊗ₜ[R] mk' A x y)
      ((algebraMap R S : (a : R) → S) (↑y : R) ⊗ₜ[R] 1 : S ⊗[R] A) =
    (algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s)
rw₄ :
  HMul.hMul (α := S ⊗[R] A) (β := S ⊗[R] A) (s ⊗ₜ[R] mk' A x y)
      (1 ⊗ₜ[R] (algebraMap R A : (a : R) → A) (↑y : R) : S ⊗[R] A) =
    (algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s)
rw₅ :
  Eq (α := S ⊗[R] A) ((s * 1) ⊗ₜ[R] HMul.hMul (β := A) (mk' A x y) ((algebraMap R A : (a : R) → A) (↑y : R) : A))
    ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s))
rw₆ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] HMul.hMul (β := A) (mk' A x y) ((algebraMap R A : (a : R) → A) (↑y : R) : A))
    ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s))
⊢ Eq (α := S ⊗[R] A) (s ⊗ₜ[R] mk' A x y)
    (mk' (M := Algebra.algebraMapSubmonoid S M) (S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
        ((algebraMap R S : (a : R) → S) (↑y : R)) ⋯))
have rw₇ : Eq (α := S ⊗[R] A) (s ⊗ₜ[R] HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (↑y : R) : A) (mk' A x y))
  ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s))
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_apply, Algebra.algebraMap_self,
    RingHomCompTriple.comp_apply, tmul_one_eq_one_tmul, tmul_mul_tmul, mul_one, mul_comm,
    IsLocalization.mk'_spec', algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]