awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ 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)
have 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
Tactic: simp only [mul_pow, pow_add, map_pow, map_mul, ← mul_assoc, hpq,
      IsScalarTower.algebraMap_apply R S T, ← hab]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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)
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
have 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)
Tactic: rw [IsScalarTower.algebraMap_apply R S T] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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)
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
have 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)
Tactic: rw [IsScalarTower.algebraMap_apply R S T] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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)
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
have 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)
Tactic: repeat rw [IsScalarTower.algebraMap_apply R S T] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
have 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
Tactic: obtain ⟨n, hn⟩ := exists_of_eq (algebraMap R S y) h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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)
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
have 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)
Tactic: simp only [← map_pow, ← map_mul, ← map_mul] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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)
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
have refine_3 : ∀ (m : ℕ) (hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)), ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
Tactic: obtain ⟨m, hm⟩ := exists_of_eq x hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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)
⊢ ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
have h₁ : (y * x) ^ (n + m) * a = (y * x) ^ (n + m) * b
Tactic: use n + m
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 * x) ^ (n + m) * b
have h₁ : (y * x) ^ (n + m) * a = y ^ m * x ^ n * (x ^ m * (y ^ n * a))
Tactic: convert_to y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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))
⊢ (y * x) ^ (n + m) * a = (y * x) ^ (n + m) * b
have h₂ : (y * x) ^ (n + m) * b = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
Tactic: convert_to y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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))
⊢ (y * x) ^ (n + m) * a = (y * x) ^ (n + m) * b
have h₃ : y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
Tactic: convert_to y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
have h₁ : y ^ m * x ^ n * (x ^ m * (y ^ n * b)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ Away.{u_6, u_8} (R := S₁) ((algebraMap R S₁ : (a : R) → S₁) y : S₁) T
have 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₁)
Tactic: convert! IsLocalization.commutes S₁ S₂ T (Submonoid.powers x) (Submonoid.powers y)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ 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₁)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ LE.le (α := Submonoid R) (Submonoid.powers x) (IsUnit.submonoid R)
have rwa : LE.le (α := Submonoid R) (Submonoid.closure {x}) (IsUnit.submonoid R)
Tactic: rwa [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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)
⊢ LE.le (α := Submonoid R) (Submonoid.powers x) (IsUnit.submonoid R)
have rwa₁ : {x} ⊆ (↑(IsUnit.submonoid R) : Set R)
Tactic: rwa [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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)
⊢ LE.le (α := Submonoid R) (Submonoid.powers x) (IsUnit.submonoid R)
have rwa₂ : x ∈ (↑(IsUnit.submonoid R) : Set R)
Tactic: rwa [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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 (x * z) T
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ ∃ (a : R), (algebraMap R S : (a : R) → S) a = x
have 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) sorry)
Tactic: obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers e) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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),
    (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) ⋯)
have suffices : ∃ (a : R) (k : ℕ), e ^ k * (a * e ^ n) = e ^ k * x
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
have refine : HPow.hPow (β := ℕ) e 1 * (x * e ^ n) = HPow.hPow (β := ℕ) e 1 * x
Tactic: refine ⟨x, 1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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) = HPow.hPow (β := ℕ) e 1 * x
have trans : HPow.hPow (β := ℕ) e 1 * (x * e ^ n) = e ^ (n + 1) * x
Tactic: trans e ^ (n + 1) * x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) e 1 * (x * e ^ n) = HPow.hPow (β := ℕ) e 1 * x
have trans₁ : e ^ (n + 1) * x = HPow.hPow (β := ℕ) e 1 * x
Tactic: trans e ^ (n + 1) * x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 ^ (n + 1) * x = HPow.hPow (β := ℕ) e 1 * x
have rw : e * x = HPow.hPow (β := ℕ) e 1 * x
Tactic: rw [he.pow_succ_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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)
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S)
have 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) sorry) :
          R) :
      S)
Tactic: obtain ⟨r, n, rfl⟩ := r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) e : S) (1 : S)
have rw : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) e : S) ((algebraMap R S : (a : R) → S) 1 : S)
Tactic: rw [← (algebraMap R S).map_one, H, mul_one, he]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) e : S) (1 : S)
have rw₁ : e * e = e * 1
Tactic: rw [← (algebraMap R S).map_one, H, mul_one, he]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) e : S) (1 : S)
have rw₂ : e * e = e
Tactic: rw [← (algebraMap R S).map_one, H, mul_one, he]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) e : S) (1 : S)
have rw₃ : e = e
Tactic: rw [← (algebraMap R S).map_one, H, mul_one, he]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨z, rfl⟩ := H' z
Cleared hypotheses: z