awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
    ((tensorRightAlgEquiv M S : (a : Localization M ⊗[R] S) → Localization (Algebra.algebraMapSubmonoid S M))
        (1 ⊗ₜ[R] x) :
      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: Quotient.liftOn', AddCon.liftOn, AlgEquiv.commutes, List.foldl, Localization.tensorLeftAlgEquiv, TensorProduct.tmul, OreLocalization.liftExpand, AddCon.toQuotient, FreeAddMonoid.sumAux
-- 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 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 (A ⊗[R] S) (B ⊗[R] S)
inst_11 : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (AlgHom.toRingHom Algebra.TensorProduct.includeRight)
⊢ IsLocalization (R := A ⊗[R] S) (Algebra.algebraMapSubmonoid (A ⊗[R] S) M) (B ⊗[R] S)

Tactic:
(Algebra.isLocalization_iff_isPushout M _).mpr
    (Algebra.IsPushout.tensorProduct_tensorProduct R S A B H).symm

Premises used: Iff.mpr, Algebra.IsPushout.tensorProduct_tensorProduct, Algebra.IsPushout.symm, Algebra.isLocalization_iff_isPushout
-- 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 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)
⊢ IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)

Tactic:
have : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B) := .of_algebraMap_eq' H.symm
-- 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 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))
rw₃ 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))
⊢ Eq (α := R →+* S ⊗[R] B) (algebraMap R (S ⊗[R] B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (S ⊗[R] B)) (algebraMap R A))

Tactic:
rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]

Premises used: RingHom.comp_assoc, IsScalarTower.algebraMap_eq, Algebra.compHom_algebraMap_eq
-- 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 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)
⊢ 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]
-- 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 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)
⊢ IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)

Tactic:
have : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B) := .to₁₃₄ _ A _ _
-- 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 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)
⊢ IsScalarTower A B (S ⊗[R] B)

Tactic:
have : IsScalarTower A B (S ⊗[R] B) := .of_algebraMap_eq' rfl
-- 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 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_4 : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower A B (S ⊗[R] B)
rw : Algebra.IsPushout R B S (S ⊗[R] B)
⊢ IsLocalization (R := S ⊗[R] A) (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)

Tactic:
rw [Algebra.isLocalization_iff_isPushout _ B, Algebra.IsPushout.comm,
    ← Algebra.IsPushout.comp_iff R _ S]

Premises used: Algebra.IsPushout.comm, Algebra.IsPushout.comp_iff, Algebra.isLocalization_iff_isPushout
-- 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 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_4 : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower A B (S ⊗[R] B)
⊢ Algebra.IsPushout R B S (S ⊗[R] B)

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'_1 : Type u_4
inst_6 : AddCommMonoid M'_1
inst_7 : Module R_1 M'_1
inst_8 : Module A_1 M'_1
inst_9 : IsScalarTower R_1 A_1 M'_1
f : M_1 →ₗ[R_1] M'_1
T : Type u_5
B_1 : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B_1
inst_12 : Algebra R_1 T
inst_13 : Algebra T B_1
inst_14 : Algebra R_1 B_1
inst_15 : Algebra A_1 B_1
inst_16 : IsScalarTower R_1 T B_1
inst_17 : IsScalarTower R_1 A_1 B_1
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 A
B : Type u_10
inst_23 : CommSemiring B
inst_24 : Algebra R B
inst_25 : Algebra A B
inst_26 : IsScalarTower R A B
inst_27 : IsLocalization M B
C : Type u_11
inst_28 : CommSemiring C
inst_29 : Algebra S C
inst_30 : Algebra (S ⊗[R] A) C
inst_31 : IsScalarTower S (S ⊗[R] A) C
inst_32 : IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B) : S ⊗[R] A →ₐ[R] S ⊗[R] B))
x : S
⊢ Eq (α := S ⊗[R] B) ((algebraMap S (S ⊗[R] B) : (a : S) → S ⊗[R] B) x : S ⊗[R] B)
    ((algebraMap (S ⊗[R] A) (S ⊗[R] B) : (a : S ⊗[R] A) → S ⊗[R] B) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) x) :
      S ⊗[R] B)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- 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'_1 : Type u_4
inst_6 : AddCommMonoid M'_1
inst_7 : Module R_1 M'_1
inst_8 : Module A_1 M'_1
inst_9 : IsScalarTower R_1 A_1 M'_1
f : M_1 →ₗ[R_1] M'_1
T : Type u_5
B_1 : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B_1
inst_12 : Algebra R_1 T
inst_13 : Algebra T B_1
inst_14 : Algebra R_1 B_1
inst_15 : Algebra A_1 B_1
inst_16 : IsScalarTower R_1 T B_1
inst_17 : IsScalarTower R_1 A_1 B_1
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 A
B : Type u_10
inst_23 : CommSemiring B
inst_24 : Algebra R B
inst_25 : Algebra A B
inst_26 : IsScalarTower R A B
inst_27 : IsLocalization M B
C : Type u_11
inst_28 : CommSemiring C
inst_29 : Algebra S C
inst_30 : Algebra (S ⊗[R] A) C
inst_31 : IsScalarTower S (S ⊗[R] A) C
inst_32 : IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M
this_1 : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B) : S ⊗[R] A →ₐ[R] S ⊗[R] B))
this : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
a :
  ∀ (x : A),
    Eq (α := S ⊗[R] B)
      ((@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
              (AlgHom.toRingHom Algebra.TensorProduct.includeRight) :
            (a : A) → S ⊗[R] B)
          x :
        S ⊗[R] B)
      ((RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B) : (a : A) → S ⊗[R] B) x :
        S ⊗[R] B)
⊢ 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))

Tactic:
ext
-- 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'_1 : Type u_4
inst_6 : AddCommMonoid M'_1
inst_7 : Module R_1 M'_1
inst_8 : Module A_1 M'_1
inst_9 : IsScalarTower R_1 A_1 M'_1
f : M_1 →ₗ[R_1] M'_1
T : Type u_5
B_1 : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B_1
inst_12 : Algebra R_1 T
inst_13 : Algebra T B_1
inst_14 : Algebra R_1 B_1
inst_15 : Algebra A_1 B_1
inst_16 : IsScalarTower R_1 T B_1
inst_17 : IsScalarTower R_1 A_1 B_1
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 A
B : Type u_10
inst_23 : CommSemiring B
inst_24 : Algebra R B
inst_25 : Algebra A B
inst_26 : IsScalarTower R A B
inst_27 : IsLocalization M B
C : Type u_11
inst_28 : CommSemiring C
inst_29 : Algebra S C
inst_30 : Algebra (S ⊗[R] A) C
inst_31 : IsScalarTower S (S ⊗[R] A) C
inst_32 : IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M
this_1 : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B) : S ⊗[R] A →ₐ[R] S ⊗[R] B))
this : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
x : A
⊢ Eq (α := S ⊗[R] B)
    ((@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
            (AlgHom.toRingHom Algebra.TensorProduct.includeRight) :
          (a : A) → S ⊗[R] B)
        x :
      S ⊗[R] B)
    ((RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B) : (a : A) → S ⊗[R] B) x :
      S ⊗[R] B)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- 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 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
C : Type u_11
inst_10 : CommSemiring C
inst_11 : Algebra S C
inst_12 : Algebra (S ⊗[R] A) C
inst_13 : IsScalarTower S (S ⊗[R] A) C
inst_14 : IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M) C
x : S
a : A
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B) : S ⊗[R] A →ₐ[R] S ⊗[R] B))
⊢ Eq (α := S ⊗[R] B) (x ⊗ₜ[R] (algebraMap A B : (a : A) → B) a : S ⊗[R] B)
    ((algebraMap (S ⊗[R] A) (S ⊗[R] B) : (a : S ⊗[R] A) → S ⊗[R] B) (x ⊗ₜ[R] a) : S ⊗[R] B)

Tactic:
have heq : x ⊗ₜ[R] (algebraMap A B) a = algebraMap _ _ (x ⊗ₜ[R] a) := rfl
-- 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 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
C : Type u_11
inst_10 : CommSemiring C
inst_11 : Algebra S C
inst_12 : Algebra (S ⊗[R] A) C
inst_13 : IsScalarTower S (S ⊗[R] A) C
inst_14 : IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M) C
x : S
a : A
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B) : S ⊗[R] A →ₐ[R] S ⊗[R] B))
heq :
  Eq (α := S ⊗[R] B) (x ⊗ₜ[R] (algebraMap A B : (a : A) → B) a : S ⊗[R] B)
    ((algebraMap (S ⊗[R] A) (S ⊗[R] B) : (a : S ⊗[R] A) → S ⊗[R] B) (x ⊗ₜ[R] a) : S ⊗[R] B)
⊢ Eq.{u_11 + 1} (α := C)
    ((tensorProductEquivOfMapIncludeRight R S M B C : (a : S ⊗[R] B) → C)
        (x ⊗ₜ[R] (algebraMap A B : (a : A) → B) a : S ⊗[R] B) :
      C)
    ((algebraMap (S ⊗[R] A) C : (a : S ⊗[R] A) → C) (x ⊗ₜ[R] a) : C)

Tactic:
simp [heq, IsLocalization.tensorProductEquivOfMapIncludeRight]

Premises used: IsLocalization.tensorProductEquivOfMapIncludeRight
-- 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 : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
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 →ₗ[R_1] M'
T : Type u_5
B_1 : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B_1
inst_12 : Algebra R_1 T
inst_13 : Algebra T B_1
inst_14 : Algebra R_1 B_1
inst_15 : Algebra A_1 B_1
inst_16 : IsScalarTower R_1 T B_1
inst_17 : IsScalarTower R_1 A_1 B_1
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
g : A
B : Type u_10
inst_23 : CommSemiring B
inst_24 : Algebra R B
inst_25 : Algebra A B
inst_26 : IsScalarTower R A B
inst_27 : Away g B
simp : IsLocalization (R := S ⊗[R] A) (Submonoid.powers (1 ⊗ₜ[R] g)) (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))
⊢ IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight (Submonoid.powers g))
    (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))

Tactic:
simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]

Premises used: Algebra.TensorProduct.includeRight_apply, Submonoid.map_powers
-- 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 : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
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 →ₗ[R_1] M'
T : Type u_5
B_1 : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B_1
inst_12 : Algebra R_1 T
inst_13 : Algebra T B_1
inst_14 : Algebra R_1 B_1
inst_15 : Algebra A_1 B_1
inst_16 : IsScalarTower R_1 T B_1
inst_17 : IsScalarTower R_1 A_1 B_1
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
g : A
B : Type u_10
inst_23 : CommSemiring B
inst_24 : Algebra R B
inst_25 : Algebra A B
inst_26 : IsScalarTower R A B
inst_27 : Away g B
⊢ IsLocalization (R := S ⊗[R] A) (Submonoid.powers (1 ⊗ₜ[R] g)) (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))

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
g : 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 : Away g B
x : S
a : A
simp : IsLocalization (R := S ⊗[R] A) (Submonoid.powers (1 ⊗ₜ[R] g)) (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))
⊢ IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight (Submonoid.powers g))
    (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))

Tactic:
simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]

Premises used: Algebra.TensorProduct.includeRight_apply, Submonoid.map_powers
-- 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
g : 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 : Away g B
x : S
a : A
⊢ IsLocalization (R := S ⊗[R] A) (Submonoid.powers (1 ⊗ₜ[R] g)) (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))

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 : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
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 →ₗ[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
inst_23 : Away r A
simp : IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (S ⊗[R] A)
⊢ Away (R := S) ((algebraMap R S : (a : R) → S) r : S) (S ⊗[R] A)

Tactic:
simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]

Premises used: IsLocalization.Away, Algebra.algebraMapSubmonoid_powers