awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
M' : Type u_4
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module A M'
inst_8 : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : Module A M
inst_12 : IsScalarTower R A M
P : Type u_8
inst_13 : AddCommMonoid P
inst_14 : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
h₁ :
  Eq (α := M ⊗[R] N →ₗ[A] M' ⊗[R] P)
    (((AlgebraTensorModule.rTensor R P : (M →ₗ[A] M') →ₗ[R] M ⊗[R] P →ₗ[A] M' ⊗[R] P) :
          (a : M →ₗ[A] M') → M ⊗[R] P →ₗ[A] M' ⊗[R] P)
        g ∘ₗ
      ((AlgebraTensorModule.lTensor A M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] P) :
          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[A] M ⊗[R] P)
        f)
    (((AlgebraTensorModule.lTensor A M' : (N →ₗ[R] P) →ₗ[R] M' ⊗[R] N →ₗ[A] M' ⊗[R] P) :
          (a : N →ₗ[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        f ∘ₗ
      ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
        g)
⊢ Eq (α := M ⊗[R] N →ₗ[A] M' ⊗[R] P)
    ((map S
            (((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
                (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
              g)
            (((AlgebraTensorModule.rTensor R P : (M →ₗ[A] M') →ₗ[R] M ⊗[R] P →ₗ[A] M' ⊗[R] P) :
                (a : M →ₗ[A] M') → M ⊗[R] P →ₗ[A] M' ⊗[R] P)
              g) :
          (a : M ⊗[R] N →ₗ[A] M ⊗[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        (((AlgebraTensorModule.lTensor A M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[A] M ⊗[R] P)
          f) ∘ₗ
      ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
        g)
    (((AlgebraTensorModule.lTensor A M' : (N →ₗ[R] P) →ₗ[R] M' ⊗[R] N →ₗ[A] M' ⊗[R] P) :
          (a : N →ₗ[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        f ∘ₗ
      ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
        g)

Tactic:
rw [map_comp]

Premises used: IsLocalizedModule.map_comp
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
M' : Type u_4
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module A M'
inst_8 : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : Module A M
inst_12 : IsScalarTower R A M
P : Type u_8
inst_13 : AddCommMonoid P
inst_14 : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
h₁ :
  ∀ (x : M) (x_1 : N),
    Eq (α := M' ⊗[R] P)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.rTensor R P : (M →ₗ[A] M') →ₗ[R] M ⊗[R] P →ₗ[A] M' ⊗[R] P) :
                            (a : M →ₗ[A] M') → M ⊗[R] P →ₗ[A] M' ⊗[R] P)
                          g ∘ₗ
                        ((AlgebraTensorModule.lTensor A M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] P) :
                            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[A] M ⊗[R] P)
                          f) :
                    M →ₗ[A] N →ₗ[R] M' ⊗[R] P) :
                  (a : M) → N →ₗ[R] M' ⊗[R] P)
                x :
              N →ₗ[R] M' ⊗[R] P) :
            (a : N) → M' ⊗[R] P)
          x_1 :
        M' ⊗[R] P)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.lTensor A M' : (N →ₗ[R] P) →ₗ[R] M' ⊗[R] N →ₗ[A] M' ⊗[R] P) :
                            (a : N →ₗ[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
                          f ∘ₗ
                        ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
                            (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
                          g) :
                    M →ₗ[A] N →ₗ[R] M' ⊗[R] P) :
                  (a : M) → N →ₗ[R] M' ⊗[R] P)
                x :
              N →ₗ[R] M' ⊗[R] P) :
            (a : N) → M' ⊗[R] P)
          x_1 :
        M' ⊗[R] P)
⊢ Eq (α := M ⊗[R] N →ₗ[A] M' ⊗[R] P)
    (((AlgebraTensorModule.rTensor R P : (M →ₗ[A] M') →ₗ[R] M ⊗[R] P →ₗ[A] M' ⊗[R] P) :
          (a : M →ₗ[A] M') → M ⊗[R] P →ₗ[A] M' ⊗[R] P)
        g ∘ₗ
      ((AlgebraTensorModule.lTensor A M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] P) :
          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[A] M ⊗[R] P)
        f)
    (((AlgebraTensorModule.lTensor A M' : (N →ₗ[R] P) →ₗ[R] M' ⊗[R] N →ₗ[A] M' ⊗[R] P) :
          (a : N →ₗ[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        f ∘ₗ
      ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
        g)

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
M' : Type u_4
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module A M'
inst_8 : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : Module A M
inst_12 : IsScalarTower R A M
P : Type u_8
inst_13 : AddCommMonoid P
inst_14 : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
x : M
x_1 : N
⊢ Eq (α := M' ⊗[R] P)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.rTensor R P : (M →ₗ[A] M') →ₗ[R] M ⊗[R] P →ₗ[A] M' ⊗[R] P) :
                          (a : M →ₗ[A] M') → M ⊗[R] P →ₗ[A] M' ⊗[R] P)
                        g ∘ₗ
                      ((AlgebraTensorModule.lTensor A M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] P) :
                          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[A] M ⊗[R] P)
                        f) :
                  M →ₗ[A] N →ₗ[R] M' ⊗[R] P) :
                (a : M) → N →ₗ[R] M' ⊗[R] P)
              x :
            N →ₗ[R] M' ⊗[R] P) :
          (a : N) → M' ⊗[R] P)
        x_1 :
      M' ⊗[R] P)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.lTensor A M' : (N →ₗ[R] P) →ₗ[R] M' ⊗[R] N →ₗ[A] M' ⊗[R] P) :
                          (a : N →ₗ[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
                        f ∘ₗ
                      ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
                          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
                        g) :
                  M →ₗ[A] N →ₗ[R] M' ⊗[R] P) :
                (a : M) → N →ₗ[R] M' ⊗[R] P)
              x :
            N →ₗ[R] M' ⊗[R] P) :
          (a : N) → M' ⊗[R] P)
        x_1 :
      M' ⊗[R] P)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A_1 : Type u_2
inst_1 : CommSemiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : IsLocalization S_1 A_1
M_1 : Type u_3
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A_1 M'
inst_9 : IsScalarTower R_1 A_1 M'
f : M_1 →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A_1 B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A_1 B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
r : R
A : Type u_9
inst_21 : CommSemiring A
inst_22 : Algebra R A
M : Submonoid R
inst_23 : IsLocalization M A
x : Algebra A (S ⊗[R] A) := Algebra.TensorProduct.rightAlgebra
rw : Algebra.IsPushout R S A (S ⊗[R] A)
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) (S ⊗[R] A)

Tactic:
rw [Algebra.isLocalization_iff_isPushout _ A]

Premises used: Algebra.isLocalization_iff_isPushout
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A_1 : Type u_2
inst_1 : CommSemiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : IsLocalization S_1 A_1
M_1 : Type u_3
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A_1 M'
inst_9 : IsScalarTower R_1 A_1 M'
f : M_1 →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A_1 B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A_1 B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
r : R
A : Type u_9
inst_21 : CommSemiring A
inst_22 : Algebra R A
M : Submonoid R
inst_23 : IsLocalization M A
x : Algebra A (S ⊗[R] A) := Algebra.TensorProduct.rightAlgebra
⊢ Algebra.IsPushout R S A (S ⊗[R] A)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A_1 : Type u_2
inst_1 : CommSemiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : IsLocalization S_1 A_1
M_1 : Type u_3
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A_1 M'
inst_9 : IsScalarTower R_1 A_1 M'
f : M_1 →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A_1 B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A_1 B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
r : R
A : Type u_9
inst_21 : CommSemiring A
inst_22 : Algebra R A
M : Submonoid R
inst_23 : IsLocalization M A
rw : Algebra.IsPushout R S A (A ⊗[R] S)
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) (A ⊗[R] S)

Tactic:
rw [Algebra.isLocalization_iff_isPushout _ A]

Premises used: Algebra.isLocalization_iff_isPushout
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A_1 : Type u_2
inst_1 : CommSemiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : IsLocalization S_1 A_1
M_1 : Type u_3
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A_1 M'
inst_9 : IsScalarTower R_1 A_1 M'
f : M_1 →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A_1 B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A_1 B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
r : R
A : Type u_9
inst_21 : CommSemiring A
inst_22 : Algebra R A
M : Submonoid R
inst_23 : IsLocalization M A
⊢ Algebra.IsPushout R S A (A ⊗[R] S)

Tactic:
infer_instance
-- 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
⊢ Eq (α := A ⊗[R] S) (mk' A x y ⊗ₜ[R] s)
    (mk' (M := Algebra.algebraMapSubmonoid S M) (A ⊗[R] S) (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:
simp [IsLocalization.eq_mk'_iff_mul_eq, map_mul,
    RingHom.algebraMap_toAlgebra]

Premises used: map_mul, RingHom.algebraMap_toAlgebra, IsLocalization.eq_mk'_iff_mul_eq
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_10
inst : CommRing R
M : Submonoid R
S : Type u_12
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
⊢ Eq.{u_12 + 1} (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M))
    ((tensorLeftAlgEquiv M S : (a : S ⊗[R] Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
        (x ⊗ₜ[R] 1) :
      Localization (M := S) (Algebra.algebraMapSubmonoid S M))
    ((algebraMap S (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
          (a : S) → Localization (Algebra.algebraMapSubmonoid S M))
        x :
      Localization (M := S) (Algebra.algebraMapSubmonoid S M))

Tactic:
(tensorLeftAlgEquiv M S).commutes x

Premises used: AlgEquiv.commutes, Localization.tensorLeftAlgEquiv, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_10
inst : CommRing R
M : Submonoid R
S : Type u_12
inst_1 : CommRing S
inst_2 : Algebra R S
x : Localization (M := R) M
Rₘ : Type u_10 := Localization (M := R) M
Sₘ : Type u_12 := Localization (M := S) (Algebra.algebraMapSubmonoid S M)
obtain :
  ∀ (x : R) (y : ↥M),
    Eq.{u_12 + 1} (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M))
      ((tensorLeftAlgEquiv M S : (a : S ⊗[R] Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
          (1 ⊗ₜ[R] IsLocalization.mk' (Localization (M := R) M) x y) :
        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))
⊢ Eq.{u_12 + 1} (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M))
    ((tensorLeftAlgEquiv M S : (a : S ⊗[R] Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
        (1 ⊗ₜ[R] x) :
      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))
        x :
      Localization (M := S) (Algebra.algebraMapSubmonoid S M))

Tactic:
obtain ⟨x, y, rfl⟩ := IsLocalization.exists_mk'_eq M x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.BaseChange
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
⊢ 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))

Tactic:
have h1 : (1 : S) ⊗ₜ[R] IsLocalization.mk' Rₘ x y = algebraMap _ _ (IsLocalization.mk' Rₘ x y) :=
    rfl
-- Module: Mathlib.RingTheory.Localization.BaseChange
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))
rw :
  (algebraMap S (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
        (a : S) → Localization (Algebra.algebraMapSubmonoid S M))
      ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) x : S)) =
    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))
          (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                ((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))
                ⋯) :
            S) :
        Localization (M := S) (Algebra.algebraMapSubmonoid S M))
⊢ Eq.{u_12 + 1} (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M))
    ((tensorLeftAlgEquiv M S : (a : S ⊗[R] Localization M) → Localization (Algebra.algebraMapSubmonoid S M))
        (1 ⊗ₜ[R] IsLocalization.mk' (Localization (M := R) M) x y) :
      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))

Tactic:
rw [h1, tensorLeftAlgEquiv, algEquiv_symm_apply,
    IsLocalization.algebraMap_mk' S, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul]

Premises used: IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul, Localization.tensorLeftAlgEquiv, IsLocalization.algebraMap_mk', Localization.algEquiv_symm_apply
-- Module: Mathlib.RingTheory.Localization.BaseChange
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))
simp_rw :
  (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))
⊢ (algebraMap S (Localization (M := S) (Algebra.algebraMapSubmonoid S M)) :
        (a : S) → Localization (Algebra.algebraMapSubmonoid S M))
      ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) x : S)) =
    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))
          (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                ((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))
                ⋯) :
            S) :
        Localization (M := S) (Algebra.algebraMapSubmonoid S M))

Tactic:
simp_rw [RingHom.id_apply]

Premises used: RingHom.id_apply
-- Module: Mathlib.RingTheory.Localization.BaseChange
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_1 : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 :
  Eq (α := S ⊗[R] Rₘ) (1 ⊗ₜ[R] IsLocalization.mk' Rₘ x_1 y)
    ((algebraMap Rₘ (S ⊗[R] Rₘ) : (a : Rₘ) → S ⊗[R] Rₘ) (IsLocalization.mk' Rₘ x_1 y))
x : R
rw :
  Eq.{u_12 + 1} (α := Sₘ) (((algebraMap R Sₘ : R →+* Sₘ) : (a : R) → Sₘ) x : Sₘ)
    (((algebraMap Rₘ Sₘ : Rₘ →+* Sₘ) : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) : Sₘ)
rw₁ rw₂ :
  Eq.{u_12 + 1} (α := Sₘ) (((algebraMap R Sₘ : R →+* Sₘ) : (a : R) → Sₘ) x : Sₘ)
    (((algebraMap R Sₘ : R →+* Sₘ) : (a : R) → Sₘ) x : Sₘ)
⊢ 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ₘ)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.BaseChange
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))
⊢ ∀ (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ₘ)

Tactic:
have h x : algebraMap S Sₘ ((algebraMap R S) x) = algebraMap Rₘ Sₘ ((algebraMap R Rₘ) x) := by
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_10
inst : CommRing R
M : Submonoid R
S : Type u_12
inst_1 : CommRing S
inst_2 : Algebra R S
x : Localization (M := R) M
⊢ Eq.{u_12 + 1} (α := Localization (M := S) (Algebra.algebraMapSubmonoid S M))
    ((tensorRightAlgEquiv M S : (a : Localization M ⊗[R] S) → Localization (Algebra.algebraMapSubmonoid S M))
        (x ⊗ₜ[R] 1) :
      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))
        x :
      Localization (M := S) (Algebra.algebraMapSubmonoid S M))

Tactic:
(tensorRightAlgEquiv M S).commutes x

Premises used: AlgEquiv.commutes, TensorProduct.tmul, AddCon.toQuotient, Localization.tensorRightAlgEquiv