-- Module: Mathlib.RingTheory.Localization.BaseChange
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))
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))
rw₈ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : 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) :
      S ⊗[R] A)
rw₉ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A)
    ((algebraMap S S : (a : S) → S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s) ⊗ₜ[R] 1 : S ⊗[R] A)
rw₁₀ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A)
    ((RingHom.id S : (a : S) → S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s) ⊗ₜ[R] 1 : S ⊗[R] A)
rw₁₁ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s ⊗ₜ[R] 1 : S ⊗[R] A)
rw₁₂ : Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A) ((x • s) ⊗ₜ[R] 1 : S ⊗[R] A)
rw₁₃ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A) (s ⊗ₜ[R] HSMul.hSMul (β := A) x 1 : S ⊗[R] A)
rw₁₄ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A)
    (s ⊗ₜ[R] HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) (1 : A) : S ⊗[R] A)
rw₁₅ rw₁₆ :
  Eq (α := S ⊗[R] A) (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A)
    (s ⊗ₜ[R] (algebraMap R A : (a : R) → A) x : S ⊗[R] A)
⊢ 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)) ⋯))

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]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, IsLocalization.mk'_spec', Algebra.TensorProduct.tmul_mul_tmul, Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHomCompTriple.comp_apply, mul_comm, Algebra.smul_def, mul_one, IsLocalization.eq_mk'_iff_mul_eq