awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ (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))
have 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))
Tactic: simp_rw [RingHom.id_apply]
-- 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_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
⊢ 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ₘ)
have 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ₘ)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
-- 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_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ₘ)
⊢ 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ₘ)
have 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ₘ)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
-- 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
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))
⊢ (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 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ₘ)
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]
-- 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ₘ)
⊢ (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 : ((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))
Tactic: rw [h, h, ← map_mul, IsLocalization.mk'_spec]
-- 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))
⊢ (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₁ : ((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ₘ)
Tactic: rw [h, h, ← map_mul, IsLocalization.mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
⊢ IsLocalization (R := S ⊗[R] A) (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)
have this₁ : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
Tactic: have : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B) := .of_algebraMap_eq' H.symm
-- 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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
⊢ Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (S ⊗[R] B)) (algebraMap R A))
have rw : Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap A B)) (algebraMap R A))
Tactic: rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]
-- 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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
rw :
  Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap A B)) (algebraMap R A))
⊢ Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (S ⊗[R] B)) (algebraMap R A))
have rw₁ : Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)))
Tactic: rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]
-- 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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
rw :
  Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap A B)) (algebraMap R A))
rw₁ :
  Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)))
⊢ Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (S ⊗[R] B)) (algebraMap R A))
have rw₂ : Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap R B))
Tactic: rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]
-- 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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
rw :
  Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap A B)) (algebraMap R A))
rw₁ :
  Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)))
rw₂ :
  Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap R B))
⊢ Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (S ⊗[R] B)) (algebraMap R A))
have rw₃ : Eq (α := R →+* S ⊗[R] B)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap R B))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B (S ⊗[R] B)) (algebraMap R B))
Tactic: rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
⊢ IsLocalization (R := S ⊗[R] A) (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)
have this₁ : IsScalarTower R A (S ⊗[R] B)
Tactic: have : IsScalarTower R A (S ⊗[R] B) :=
    .of_algebraMap_eq' <| by
      rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this_2 : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower R A (S ⊗[R] B)
⊢ IsLocalization (R := S ⊗[R] A) (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)
have this₁ : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
Tactic: have : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B) := .to₁₃₄ _ A _ _
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
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 A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this_2 : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
this_3 : IsScalarTower R A (S ⊗[R] B)
this : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
⊢ IsLocalization (R := S ⊗[R] A) (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)
have this₁ : IsScalarTower A B (S ⊗[R] B)
Tactic: have : IsScalarTower A B (S ⊗[R] B) := .of_algebraMap_eq' rfl