awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) (S ⊗[R] A)
have rw : Algebra.IsPushout R S A (S ⊗[R] A)
Tactic: rw [Algebra.isLocalization_iff_isPushout _ A]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) (A ⊗[R] S)
have rw : Algebra.IsPushout R S A (A ⊗[R] S)
Tactic: rw [Algebra.isLocalization_iff_isPushout _ A]
-- 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
⊢ 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 : 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)) sorry) :
          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)
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]
-- 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)
⊢ 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₁ : 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)) sorry) :
              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)
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]
-- 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)
⊢ 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₂ : 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)) sorry) :
              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)
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]
-- 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)
⊢ 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₃ : 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)
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]
-- 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)
⊢ 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₄ : 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)
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]
-- 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)
⊢ 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 * 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))
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]
-- 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
x : Localization (M := R) M
Rₘ : Type u_10 := Localization (M := R) M
Sₘ : Type u_12 := 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))
have 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))
Tactic: obtain ⟨x, y, rfl⟩ := IsLocalization.exists_mk'_eq M x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
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.{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))
have 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))
Tactic: have h1 : (1 : S) ⊗ₜ[R] IsLocalization.mk' Rₘ x y = algebraMap _ _ (IsLocalization.mk' Rₘ x y) :=
    rfl
-- 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))
⊢ 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))
have 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)) sorry) :
                    S) :
                  S))
              sorry) :
          S) :
      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]