-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_10
inst : CommRing R
M : Submonoid R
S : Type u_12
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_10 := Localization (M := R) M
Sₘ : Type u_12 := Localization (M := S) (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 :
  Eq (α := S ⊗[R] Rₘ) (1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y)
    ((algebraMap Rₘ (S ⊗[R] Rₘ) : (a : Rₘ) → S ⊗[R] Rₘ) (IsLocalization.mk' Rₘ x y))
h :
  ∀ (x : R),
    Eq (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) x) : Sₘ)
      (((algebraMap Rₘ Sₘ : Rₘ →+* Sₘ) : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) : Sₘ)
rw :
  ((algebraMap Rₘ Sₘ : Rₘ →+* Sₘ) : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) =
    HMul.hMul (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M)) (β :=
      Localization (M := S) (Algebra.algebraMapSubmonoid S M))
      ((algebraMap (Localization (M := R) M) (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
            (a : Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
          (IsLocalization.mk' (Localization (M := R) M) x y) :
        Localization (M := S) (Algebra.algebraMapSubmonoid S M))
      ((algebraMap S (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
            (a : S) → Localization (Algebra.algebraMapSubmonoid S M))
          ((algebraMap R S : (a : R) → S) (↑y : R)) :
        Localization (M := S) (Algebra.algebraMapSubmonoid S M))
rw₁ :
  ((algebraMap Rₘ Sₘ : Rₘ →+* Sₘ) : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) =
    HMul.hMul (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M)) (β :=
      Localization (M := S) (Algebra.algebraMapSubmonoid S M))
      ((algebraMap (Localization (M := R) M) (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
            (a : Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
          (IsLocalization.mk' (Localization (M := R) M) x y) :
        Localization (M := S) (Algebra.algebraMapSubmonoid S M))
      (((algebraMap Rₘ Sₘ : Rₘ →+* Sₘ) : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑y : R)) : Sₘ)
⊢ (algebraMap S (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
        (a : S) → Localization (Algebra.algebraMapSubmonoid S M))
      ((algebraMap R S : (a : R) → S) x) =
    HMul.hMul (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M)) (β :=
      Localization (M := S) (Algebra.algebraMapSubmonoid S M))
      ((algebraMap (Localization (M := R) M) (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
            (a : Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
          (IsLocalization.mk' (Localization (M := R) M) x y) :
        Localization (M := S) (Algebra.algebraMapSubmonoid S M))
      ((algebraMap S (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
            (a : S) → Localization (Algebra.algebraMapSubmonoid S M))
          ((algebraMap R S : (a : R) → S) (↑y : R)) :
        Localization (M := S) (Algebra.algebraMapSubmonoid S M))
have rw₂ : Eq.{u_12 + 1} (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M))
  (((algebraMap Rₘ Sₘ : Rₘ →+* Sₘ) : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) : Sₘ)
  ((algebraMap (Localization (M := R) M) (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
        (a : Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
      (HMul.hMul (α := Localization (M := R) M) (β := Localization (M := R) M)
        (IsLocalization.mk' (Localization (M := R) M) x y : Localization (M := R) M)
        ((algebraMap R Rₘ : (a : R) → Rₘ) (↑y : R) : Rₘ)) :
    Localization (M := S) (Algebra.algebraMapSubmonoid S M))
Tactic: rw [h, h, ← map_mul, IsLocalization.mk'_spec]