awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ^ m * x ^ n * (x ^ m * (y ^ n * a))
h₂ : (y * x) ^ (n + m) * b = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
h₃ : y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
⊢ (y * x) ^ (n + m) * a = (y * x) ^ (n + m) * b

Tactic:
convert_to y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

Premises used: HMul.hMul, HPow.hPow
-- 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)
⊢ (y * x) ^ (n + m) * a = y ^ m * x ^ n * (x ^ m * (y ^ n * a))

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 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)
⊢ (y * x) ^ (n + m) * b = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

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 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₁ h₂ : y ^ m * x ^ n * (x ^ m * (y ^ n * b)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
⊢ y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

Tactic:
rw [hm]
-- 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 (x * y) T

Tactic:
mul_comm x y ▸ mul S T x y

Premises used: IsLocalization.Away.mul, Eq.rec, mul_comm, Eq.symm
-- 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_1 : R
inst_4 : Away x_1 S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
x y : R
inst_7 : Away x S
⊢ Away.{u_1, u_2} (y * x) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) y : S))

Tactic:
IsLocalization.Away.mul S (Localization.Away (algebraMap R S y)) _ _

Premises used: Algebra.algebraMap, Localization.Away, IsLocalization.Away.mul, DFunLike.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_1 : R
inst_4 : Away x_1 S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
x y : R
inst_7 : Away x S
⊢ Away.{u_1, u_2} (x * y) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) y : S))

Tactic:
IsLocalization.Away.mul' S (Localization.Away (algebraMap R S y)) _ _

Premises used: Algebra.algebraMap, Localization.Away, IsLocalization.Away.mul', DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_5
inst : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
x y : R
inst_11 : Away x S₁
inst_12 : Away y S₂
inst_13 : Away.{u_7, u_8} (R := S₂) ((algebraMap R S₂ : (a : R) → S₂) x : S₂) T
⊢ IsLocalization (Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)) T

Tactic:
IsLocalization.commutes S₁ S₂ T (Submonoid.powers x) (Submonoid.powers y)

Premises used: IsLocalization.commutes, Submonoid.powers
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_5
inst : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
x y : R
inst_11 : Away x S₁
inst_12 : Away y S₂
inst_13 : Away.{u_7, u_8} (R := S₂) ((algebraMap R S₂ : (a : R) → S₂) x : S₂) T
h :
  Eq.{u_6 + 1} (α := Submonoid S₁) (Submonoid.powers ((algebraMap R S₁ : (a : R) → S₁) y) : Submonoid S₁)
    (Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y) : Submonoid S₁)
⊢ Away.{u_6, u_8} (R := S₁) ((algebraMap R S₁ : (a : R) → S₁) y : S₁) T

Tactic:
convert! IsLocalization.commutes S₁ S₂ T (Submonoid.powers x) (Submonoid.powers y)

Premises used: IsLocalization.commutes, Submonoid.powers
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_5
inst : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
x y : R
inst_11 : Away x S₁
inst_12 : Away y S₂
inst_13 : Away.{u_7, u_8} (R := S₂) ((algebraMap R S₂ : (a : R) → S₂) x : S₂) T
h :
  ∀ (x : S₁),
    Membership.mem (γ := Submonoid S₁) (Submonoid.powers ((algebraMap R S₁ : (a : R) → S₁) y) : Submonoid S₁) x ↔
      Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)) x
⊢ Eq.{u_6 + 1} (α := Submonoid S₁) (Submonoid.powers ((algebraMap R S₁ : (a : R) → S₁) y) : Submonoid S₁)
    (Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y) : Submonoid S₁)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_5
inst : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
x_1 y : R
inst_11 : Away x_1 S₁
inst_12 : Away y S₂
inst_13 : Away.{u_7, u_8} (R := S₂) ((algebraMap R S₂ : (a : R) → S₂) x_1 : S₂) T
x : S₁
⊢ Membership.mem (γ := Submonoid S₁) (Submonoid.powers ((algebraMap R S₁ : (a : R) → S₁) y) : Submonoid S₁) x ↔
    Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)) x

Tactic:
simp
-- 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
inst_4 : IsLocalization M S
x : R
e : IsUnit x
inst_5 : Away x S
rwa : LE.le (α := Submonoid R) (Submonoid.closure {x}) (IsUnit.submonoid R)
rwa₁ : {x} ⊆ (↑(IsUnit.submonoid R) : Set R)
rwa₂ rwa₃ rwa₄ rwa₅ : x ∈ (↑(IsUnit.submonoid R) : Set R)
⊢ LE.le (α := Submonoid R) (Submonoid.powers x) (IsUnit.submonoid R)

Tactic:
rwa [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Submonoid.powers_eq_closure, Submonoid.closure_le
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (IsUnit.submonoid S)

Tactic:
simpa [Submonoid.powers_le] using hr.map (algebraMap R S)

Premises used: Algebra.algebraMap, IsUnit.map, Submonoid.powers_le
-- 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
x y : R
inst_3 : Away x S
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) y : S)
⊢ Away (x * y) S

Tactic:
have : Away (algebraMap R S y) S := away_of_isUnit_of_bijective _ h Function.bijective_id
  .mul' S _ _ _

Premises used: Function.bijective_id, IsLocalization.away_of_isUnit_of_bijective, IsLocalization.Away.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
x y : R
inst_3 : Away y S
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
⊢ Away (x * y) S

Tactic:
have : Away (algebraMap R S x) S := away_of_isUnit_of_bijective _ h Function.bijective_id
  .mul S _ _ _

Premises used: Function.bijective_id, IsLocalization.Away.mul, IsLocalization.away_of_isUnit_of_bijective
-- 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
x z : R
y : S
inst_3 : Away x S
T : Type u_4
inst_4 : CommRing T
inst_5 : Algebra S T
inst_6 : Algebra R T
inst_7 : IsScalarTower R S T
inst_8 : Away y T
h : Associated ((algebraMap R S : (a : R) → S) z) y
rwa rwa₁ rwa₂ rwa₃ : Away y T
⊢ Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) z : S) T

Tactic:
rwa [iff_of_associated h]

Premises used: IsLocalization.Away.iff_of_associated
-- 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
x z : R
y : S
inst_3 : Away x S
T : Type u_4
inst_4 : CommRing T
inst_5 : Algebra S T
inst_6 : Algebra R T
inst_7 : IsScalarTower R S T
inst_8 : Away y T
h : Associated ((algebraMap R S : (a : R) → S) z) y
⊢ Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) z : S) T

Tactic:
have : Away (algebraMap R S z) T := by rwa [iff_of_associated h]
-- 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
x z : R
y : S
inst_3 : Away x S
T : Type u_4
inst_4 : CommRing T
inst_5 : Algebra S T
inst_6 : Algebra R T
inst_7 : IsScalarTower R S T
inst_8 : Away y T
h : Associated ((algebraMap R S : (a : R) → S) z) y
this : Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) z : S) T
⊢ Away (x * z) T

Tactic:
.mul' S _ _ _

Premises used: IsLocalization.Away.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
x z : R
y : S
inst_3 : Away x S
T : Type u_4
inst_4 : CommRing T
inst_5 : Algebra S T
inst_6 : Algebra R T
inst_7 : IsScalarTower R S T
inst_8 : Away y T
h : Associated ((algebraMap R S : (a : R) → S) z) y
this : Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) z : S) T
⊢ Away (x * z) T

Tactic:
exact .mul' S _ _ _
-- 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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : S
obtain :
  ∀ (x : R) (n : ℕ),
    ∃ (a : R),
      (algebraMap R S : (a : R) → S) a =
        mk' S x
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers e) x)
            ((fun (x : ℕ) ↦ e ^ x) n) ⋯)
⊢ ∃ (a : R), (algebraMap R S : (a : R) → S) a = x

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers e) x

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
this : ∃ (a : R) (k : ℕ), e ^ k * (a * e ^ n) = e ^ k * x
⊢ ∃ (a : R),
    (algebraMap R S : (a : R) → S) a =
      mk' S x
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers e) x)
          ((fun (x : ℕ) ↦ e ^ x) n) ⋯)

Tactic:
simpa [IsLocalization.eq_mk'_iff_mul_eq, ← map_pow, ← map_mul,
      IsLocalization.eq_iff_exists (.powers e), Submonoid.mem_powers_iff]

Premises used: map_pow, map_mul, Submonoid.powers, Submonoid.mem_powers_iff, IsLocalization.eq_mk'_iff_mul_eq, IsLocalization.eq_iff_exists
-- 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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
suffices : ∃ (a : R) (k : ℕ), e ^ k * (a * e ^ n) = e ^ k * x
⊢ ∃ (a : R),
    (algebraMap R S : (a : R) → S) a =
      mk' S x
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers e) x)
          ((fun (x : ℕ) ↦ e ^ x) n) ⋯)

Tactic:
suffices ∃ a k, e ^ k * (a * e ^ n) = e ^ k * x by
    simpa [IsLocalization.eq_mk'_iff_mul_eq, ← map_pow, ← map_mul,
      IsLocalization.eq_iff_exists (.powers e), Submonoid.mem_powers_iff]
-- 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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
⊢ ∃ (a : R) (k : ℕ), e ^ k * (a * e ^ n) = e ^ k * x

Tactic:
⟨x, 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- 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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
refine : HPow.hPow (β := ℕ) e 1 * (x * e ^ n) = HPow.hPow (β := ℕ) e 1 * x
⊢ ∃ (a : R) (k : ℕ), e ^ k * (a * e ^ n) = e ^ k * x

Tactic:
refine ⟨x, 1, ?_⟩
-- 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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
trans : HPow.hPow (β := ℕ) e 1 * (x * e ^ n) = e ^ (n + 1) * x
trans₁ : e ^ (n + 1) * x = HPow.hPow (β := ℕ) e 1 * x
⊢ HPow.hPow (β := ℕ) e 1 * (x * e ^ n) = HPow.hPow (β := ℕ) e 1 * x

Tactic:
trans e ^ (n + 1) * x

Premises used: HAdd.hAdd, OfNat.ofNat
-- 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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
⊢ HPow.hPow (β := ℕ) e 1 * (x * e ^ n) = e ^ (n + 1) * x

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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
rw : e * x = HPow.hPow (β := ℕ) e 1 * x
⊢ e ^ (n + 1) * x = HPow.hPow (β := ℕ) e 1 * x

Tactic:
rw [he.pow_succ_eq]

Premises used: IsIdempotentElem.pow_succ_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
e : R
he : IsIdempotentElem e
inst_3 : Away e S
x : R
n : ℕ
⊢ e * x = HPow.hPow (β := ℕ) e 1 * x

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
e : R
he : IsIdempotentElem e
H :
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y
H' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : ↥(Submonoid.powers e)
obtain :
  ∀ (n : ℕ),
    IsUnit (M := S)
      ((algebraMap R S : (a : R) → S)
          (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers e) x)
                ((fun (x : ℕ) ↦ e ^ x) n) ⋯) :
            R) :
        S)
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S)

Tactic:
obtain ⟨r, n, rfl⟩ := r

Premises used: rfl
-- 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
e : R
he : IsIdempotentElem e
H :
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y
H' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
n : ℕ
rw : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) e : S) ((algebraMap R S : (a : R) → S) 1 : S)
rw₁ : e * e = e * 1
rw₂ : e * e = e
rw₃ rw₄ : e = e
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) e : S) (1 : S)

Tactic:
rw [← (algebraMap R S).map_one, H, mul_one, he]

Premises used: Algebra.algebraMap, RingHom.map_one, mul_one
-- 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
e : R
he : IsIdempotentElem e
H :
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y
H' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
n : ℕ
⊢ IsUnit (M := S)
    ((algebraMap R S : (a : R) → S)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers e) x)
              ((fun (x : ℕ) ↦ e ^ x) n) ⋯) :
          R) :
      S)

Tactic:
simp [show algebraMap R S e = 1 by rw [← (algebraMap R S).map_one, H, mul_one, he]]
-- 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
e : R
he : IsIdempotentElem e
H :
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y
H' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
z : S
obtain :
  ∀ (z : R),
    ∃ (x : R × ↥(Submonoid.powers e)),
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S)
          ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
        (algebraMap R S : (a : R) → S) x.1
⊢ ∃ (x : R × ↥(Submonoid.powers e)),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1

Tactic:
obtain ⟨z, rfl⟩ := H' z

Premises used: rfl
-- 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
e : R
he : IsIdempotentElem e
H :
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y
H' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
z : R
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S)
      ((algebraMap R S : (a : R) → S) (↑(z, 1).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (z, 1).1

Tactic:
simp
-- 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
e : R
he : IsIdempotentElem e
H :
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y
H' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
z : R
⊢ ∃ (x : R × ↥(Submonoid.powers e)),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
      (algebraMap R S : (a : R) → S) x.1

Tactic:
exact ⟨⟨z, 1⟩, by simp⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
e : R
he : IsIdempotentElem e
H : Eq (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S)) (Ideal.span {1 - e})
H' : Function.Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x y : R
rw : x • e = y • e ↔ e * x = e * y
⊢ Eq.{u_5 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y

Tactic:
rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, H, ← he.ker_toSpanSingleton_eq_span,
      LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, sub_smul, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, IsIdempotentElem.ker_toSpanSingleton_eq_span, RingHom.mem_ker, sub_smul, LinearMap.toSpanSingleton_apply, LinearMap.mem_ker
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
e : R
he : IsIdempotentElem e
H : Eq (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S)) (Ideal.span {1 - e})
H' : Function.Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x y : R
simp_rw : x • e = y • e ↔ x * e = y * e
⊢ x • e = y • e ↔ e * x = e * y

Tactic:
simp_rw [mul_comm e, smul_eq_mul]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
fst : (HMul.hMul (α := R × S) (1, 0) (1, 0)).1 = (1, 0).1
snd : (HMul.hMul (α := R × S) (1, 0) (1, 0)).2 = (1, 0).2
⊢ IsIdempotentElem (M := R × S) (1, 0)

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
⊢ (HMul.hMul (α := R × S) (1, 0) (1, 0)).1 = (1, 0).1

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
⊢ (HMul.hMul (α := R × S) (1, 0) (1, 0)).2 = (1, 0).2

Tactic:
simp