awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
A : Type u_5
inst_7 : CommSemiring A
inst_8 : Algebra R A
B : Type u_6
inst_9 : CommSemiring B
inst_10 : Algebra R B
Aₚ : Type u_7
inst_11 : CommSemiring Aₚ
inst_12 : Algebra A Aₚ
inst_13 : Algebra R Aₚ
inst_14 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_15 : CommSemiring Bₚ
inst_16 : Algebra B Bₚ
inst_17 : Algebra R Bₚ
inst_18 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_19 : Away a Aₚ
inst_20 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
r : R
dsimp :
  Eq.{u_8 + 1} (α := Bₚ)
    (((↑(↑(IsLocalization.map (T := Submonoid.powers ((f : (a : A) → B) a)) Bₚ (↑f : A →+* B) ⋯) : Aₚ →* Bₚ) :
            OneHom Aₚ Bₚ) :
          (a : Aₚ) → Bₚ)
        ((algebraMap R Aₚ : (a : R) → Aₚ) r : Aₚ) :
      Bₚ)
    ((algebraMap R Bₚ : (a : R) → Bₚ) r : Bₚ)
⊢ OneHom.toFun (↑(↑(map Aₚ Bₚ f.toRingHom a) : Aₚ →* Bₚ) : OneHom Aₚ Bₚ) ((algebraMap R Aₚ : (a : R) → Aₚ) r) =
    (algebraMap R Bₚ : (a : R) → Bₚ) r

Tactic:
dsimp only [AlgHom.toRingHom_eq_coe, map, RingHom.coe_coe, OneHom.toFun_eq_coe]

Premises used: RingHom.coe_coe, IsLocalization.Away.map, AlgHom.toRingHom_eq_coe, OneHom.toFun_eq_coe
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
A : Type u_5
inst_7 : CommSemiring A
inst_8 : Algebra R A
B : Type u_6
inst_9 : CommSemiring B
inst_10 : Algebra R B
Aₚ : Type u_7
inst_11 : CommSemiring Aₚ
inst_12 : Algebra A Aₚ
inst_13 : Algebra R Aₚ
inst_14 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_15 : CommSemiring Bₚ
inst_16 : Algebra B Bₚ
inst_17 : Algebra R Bₚ
inst_18 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_19 : Away a Aₚ
inst_20 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
r : R
rw :
  Eq.{u_8 + 1} (α := Bₚ)
    (((↑(↑(IsLocalization.map (T := Submonoid.powers ((f : (a : A) → B) a)) Bₚ (↑f : A →+* B) ⋯) : Aₚ →* Bₚ) :
            OneHom Aₚ Bₚ) :
          (a : Aₚ) → Bₚ)
        ((algebraMap A Aₚ : (a : A) → Aₚ) ((algebraMap R A : (a : R) → A) r : A) : Aₚ) :
      Bₚ)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B Bₚ) (algebraMap R B) : (a : R) → Bₚ) r : Bₚ)
⊢ Eq.{u_8 + 1} (α := Bₚ)
    (((↑(↑(IsLocalization.map (T := Submonoid.powers ((f : (a : A) → B) a)) Bₚ (↑f : A →+* B) ⋯) : Aₚ →* Bₚ) :
            OneHom Aₚ Bₚ) :
          (a : Aₚ) → Bₚ)
        ((algebraMap R Aₚ : (a : R) → Aₚ) r : Aₚ) :
      Bₚ)
    ((algebraMap R Bₚ : (a : R) → Bₚ) r : Bₚ)

Tactic:
rw [IsScalarTower.algebraMap_apply R A Aₚ, IsScalarTower.algebraMap_eq R B Bₚ]

Premises used: IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
A : Type u_5
inst_7 : CommSemiring A
inst_8 : Algebra R A
B : Type u_6
inst_9 : CommSemiring B
inst_10 : Algebra R B
Aₚ : Type u_7
inst_11 : CommSemiring Aₚ
inst_12 : Algebra A Aₚ
inst_13 : Algebra R Aₚ
inst_14 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_15 : CommSemiring Bₚ
inst_16 : Algebra B Bₚ
inst_17 : Algebra R Bₚ
inst_18 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_19 : Away a Aₚ
inst_20 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
r : R
⊢ Eq.{u_8 + 1} (α := Bₚ)
    (((↑(↑(IsLocalization.map (T := Submonoid.powers ((f : (a : A) → B) a)) Bₚ (↑f : A →+* B) ⋯) : Aₚ →* Bₚ) :
            OneHom Aₚ Bₚ) :
          (a : Aₚ) → Bₚ)
        ((algebraMap A Aₚ : (a : A) → Aₚ) ((algebraMap R A : (a : R) → A) r : A) : Aₚ) :
      Bₚ)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B Bₚ) (algebraMap R B) : (a : R) → Bₚ) r : Bₚ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommSemiring B
inst_4 : Algebra R B
Aₚ : Type u_7
inst_5 : CommSemiring Aₚ
inst_6 : Algebra A Aₚ
inst_7 : Algebra R Aₚ
inst_8 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_9 : CommSemiring Bₚ
inst_10 : Algebra B Bₚ
inst_11 : Algebra R Bₚ
inst_12 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_13 : Away a Aₚ
inst_14 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
x : Aₚ
⊢ Eq.{u_8 + 1} (α := Bₚ) ((mapₐ Aₚ Bₚ f a : (a : Aₚ) → Bₚ) x : Bₚ) ((map Aₚ Bₚ f.toRingHom a : (a : Aₚ) → Bₚ) x : Bₚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommSemiring B
inst_4 : Algebra R B
Aₚ : Type u_7
inst_5 : CommSemiring Aₚ
inst_6 : Algebra A Aₚ
inst_7 : Algebra R Aₚ
inst_8 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_9 : CommSemiring Bₚ
inst_10 : Algebra B Bₚ
inst_11 : Algebra R Bₚ
inst_12 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_13 : Away a Aₚ
inst_14 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
hf : Function.Injective.{u_5 + 1, u_6 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective.{u_7 + 1, u_8 + 1} (α := Aₚ) (β := Bₚ) (⇑(mapₐ Aₚ Bₚ f a) : (a : Aₚ) → Bₚ)

Tactic:
IsLocalization.map_injective_of_injective _ _ _ hf

Premises used: IsLocalization.map_injective_of_injective
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommSemiring B
inst_4 : Algebra R B
Aₚ : Type u_7
inst_5 : CommSemiring Aₚ
inst_6 : Algebra A Aₚ
inst_7 : Algebra R Aₚ
inst_8 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_9 : CommSemiring Bₚ
inst_10 : Algebra B Bₚ
inst_11 : Algebra R Bₚ
inst_12 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_13 : Away a Aₚ
inst_14 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
simp : IsLocalization.{u_6, u_8} (R := B) (Submonoid.powers ((f : (a : A) → B) a) : Submonoid B) Bₚ
⊢ IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ

Tactic:
simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe]

Premises used: RingHom.coe_coe, AlgHom.toRingHom_eq_coe, Submonoid.map_powers
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommSemiring B
inst_4 : Algebra R B
Aₚ : Type u_7
inst_5 : CommSemiring Aₚ
inst_6 : Algebra A Aₚ
inst_7 : Algebra R Aₚ
inst_8 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_9 : CommSemiring Bₚ
inst_10 : Algebra B Bₚ
inst_11 : Algebra R Bₚ
inst_12 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_13 : Away a Aₚ
inst_14 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ IsLocalization.{u_6, u_8} (R := B) (Submonoid.powers ((f : (a : A) → B) a) : Submonoid B) Bₚ

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
⊢ Away (y * x) T

Tactic:
mk _ ?_ (fun z ↦ ?_) (fun a b h ↦ ?_)

Premises used: IsLocalization.Away.mk
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
refine_1 : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) (y * x) : T)
refine_2 :
  ∀ (z : T),
    ∃ (n : ℕ) (a : R),
      z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
refine_3 :
  ∀ (a b : R) (h : Eq.{u_5 + 1} (α := T) ((algebraMap R T : (a : R) → T) a : T) ((algebraMap R T : (a : R) → T) b : T)),
    ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
⊢ Away (y * x) T

Tactic:
refine mk _ ?_ (fun z ↦ ?_) (fun a b h ↦ ?_)

Premises used: IsLocalization.Away.mk
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
refine_1 :
  IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) ∧
    IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
⊢ IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) (y * x) : T)

Tactic:
simp only [map_mul, IsUnit.mul_iff, IsScalarTower.algebraMap_apply R S T]

Premises used: IsUnit.mul_iff, map_mul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
⊢ IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) ∧
    IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)

Tactic:
⟨algebraMap_isUnit _, IsUnit.map _ (algebraMap_isUnit x)⟩

Premises used: And.intro, IsUnit.map, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
⊢ IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) ∧
    IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)

Tactic:
exact ⟨algebraMap_isUnit _, IsUnit.map _ (algebraMap_isUnit x)⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
refine_2 :
  ∀ (m : ℕ) (p : S)
    (hpq :
      z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
        (algebraMap S T : (a : S) → T) p),
    ∃ (n : ℕ) (a : R),
      z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
⊢ ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a

Tactic:
obtain ⟨m, p, hpq⟩ := surj (algebraMap R S y) z

Premises used: Algebra.algebraMap, IsLocalization.Away.surj, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
m : ℕ
p : S
hpq :
  z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
    (algebraMap S T : (a : S) → T) p
refine_2 :
  ∀ (n : ℕ) (a : R)
    (hab : p * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a),
    ∃ (n : ℕ) (a : R),
      z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
⊢ ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a

Tactic:
obtain ⟨n, a, hab⟩ := surj x p

Premises used: IsLocalization.Away.surj
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
m : ℕ
p : S
hpq :
  z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
    (algebraMap S T : (a : S) → T) p
n : ℕ
a : R
hab : p * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
h :
  z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) (m + n) =
    (algebraMap R T : (a : R) → T) (a * x ^ m * y ^ n)
⊢ ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a

Tactic:
use m + n, a * x ^ m * y ^ n
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
m : ℕ
p : S
hpq :
  z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
    (algebraMap S T : (a : S) → T) p
n : ℕ
a : R
hab : p * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
h :
  HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) p : T)
          (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) m) *
        HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) n *
      HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) n =
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) p : T)
          (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) n) *
        HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) m *
      HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) n
⊢ z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) (m + n) =
    (algebraMap R T : (a : R) → T) (a * x ^ m * y ^ n)

Tactic:
simp only [mul_pow, pow_add, map_pow, map_mul, ← mul_assoc, hpq,
      IsScalarTower.algebraMap_apply R S T, ← hab]

Premises used: mul_assoc, pow_add, map_pow, map_mul, mul_pow, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
m : ℕ
p : S
hpq :
  z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
    (algebraMap S T : (a : S) → T) p
n : ℕ
a : R
hab : p * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
⊢ HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) p : T)
          (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) m) *
        HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) n *
      HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) n =
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) p : T)
          (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) n) *
        HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) m *
      HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) n

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
a b : R
h : Eq.{u_5 + 1} (α := T) ((algebraMap R T : (a : R) → T) a : T) ((algebraMap R T : (a : R) → T) b : T)
⊢ Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap R T : (a : R) → T) b : T)

Tactic:
rw [IsScalarTower.algebraMap_apply R S T] at h

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
a b : R
h :
  Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap R T : (a : R) → T) b : T)
⊢ Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) b : S) : T)

Tactic:
rw [IsScalarTower.algebraMap_apply R S T] at h

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
a b : R
h : Eq.{u_5 + 1} (α := T) ((algebraMap R T : (a : R) → T) a : T) ((algebraMap R T : (a : R) → T) b : T)
⊢ Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) b : S) : T)

Tactic:
repeat rw [IsScalarTower.algebraMap_apply R S T] at h

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
a b : R
h :
  Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) b : S) : T)
refine_3 :
  ∀ (n : ℕ)
    (hn :
      HMul.hMul (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) y : S) n)
          ((algebraMap R S : (a : R) → S) a : S) =
        HMul.hMul (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) y : S) n)
          ((algebraMap R S : (a : R) → S) b : S)),
    ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
obtain ⟨n, hn⟩ := exists_of_eq (algebraMap R S y) h

Premises used: Algebra.algebraMap, IsLocalization.Away.exists_of_eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
a b : R
h :
  Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) b : S) : T)
n : ℕ
hn :
  HMul.hMul (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) y : S) n)
      ((algebraMap R S : (a : R) → S) a : S) =
    HMul.hMul (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) y : S) n)
      ((algebraMap R S : (a : R) → S) b : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (y ^ n * a) : S)
    ((algebraMap R S : (a : R) → S) (y ^ n * b) : S)

Tactic:
simp only [← map_pow, ← map_mul, ← map_mul] at hn

Premises used: map_pow, map_mul
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
a b : R
h :
  Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) b : S) : T)
n : ℕ
hn :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (y ^ n * a) : S)
    ((algebraMap R S : (a : R) → S) (y ^ n * b) : S)
refine_3 : ∀ (m : ℕ) (hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)), ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
obtain ⟨m, hm⟩ := exists_of_eq x hn

Premises used: IsLocalization.Away.exists_of_eq
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
a b : R
h :
  Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) b : S) : T)
n : ℕ
hn :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (y ^ n * a) : S)
    ((algebraMap R S : (a : R) → S) (y ^ n * b) : S)
m : ℕ
hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)
h₁ : (y * x) ^ (n + m) * a = (y * x) ^ (n + m) * b
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
use n + m