awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : (↑(p.primesOver S) : Type u_2)
h :
  LE.le.{u_4} (α := (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
    (({
            toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
            invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
              Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
        Q :
      (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
    (({
            toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
            invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
              Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
        Q' :
      (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
⊢ Q ≤ Q'
have this : (↑Q' : Ideal S).IsMaximal
Tactic: have : Q'.1.IsMaximal :=
      (primesOver.isPrime p Q').isMaximal (ne_bot_of_mem_primesOver hp Q'.prop)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
⊢ inertiaDeg.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ)
      (↑((primesOverEquivPrimesOver p Rₚ Sₚ hp :
              (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
            P) :
        Ideal Sₚ) =
    p.inertiaDeg (↑P : Ideal S)
have this : NeZero p
Tactic: have : NeZero p := ⟨hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this : NeZero p
⊢ inertiaDeg.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ)
      (↑((primesOverEquivPrimesOver p Rₚ Sₚ hp :
              (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
            P) :
        Ideal Sₚ) =
    p.inertiaDeg (↑P : Ideal S)
have this₁ : (↑P : Ideal S).IsMaximal
Tactic: have : P.val.IsMaximal := Ring.DimensionLEOne.maximalOfPrime
    (ne_bot_of_mem_primesOver (NeZero.ne _) P.prop) inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this_1 : NeZero p
this : (↑P : Ideal S).IsMaximal
⊢ inertiaDeg.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ)
      (↑((primesOverEquivPrimesOver p Rₚ Sₚ hp :
              (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
            P) :
        Ideal Sₚ) =
    p.inertiaDeg (↑P : Ideal S)
have this₁ : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) (maximalIdeal Rₚ)
Tactic: have : (P.1.map (algebraMap S Sₚ)).LiesOver (maximalIdeal Rₚ) := liesOver_map_of_liesOver p _ _ _
-- 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
x : R
inst_3 : Away x S
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) (invSelf x : S) = 1
have h : (algebraMap R S : (a : R) → S) x =
  mk' (M := Submonoid.powers x) S
    (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x sorry) : R) 1
Tactic: convert! IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 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
x : R
inst_3 : Away x S
⊢ (algebraMap R S : (a : R) → S) x =
    mk' (M := Submonoid.powers x) S
      (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x ⋯) : R) 1
have h : mk' (M := Submonoid.powers x) S
    (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x sorry) : R) 1 =
  (algebraMap R S : (a : R) → S) x
Tactic: symm
-- 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
x : R
inst_3 : Away x S
s : S
⊢ HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (x ^ (sec x s).2) : S) =
    (algebraMap R S : (a : R) → S) (sec x s).1
have simp : HMul.hMul (β := S) s
    ((algebraMap R S : (a : R) → S)
        (x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) sorry) :
      S) =
  HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R) : S)
Tactic: simp only [IsLocalization.Away.sec, ← IsLocalization.sec_spec]
-- 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
x : R
inst_3 : Away x S
s : S
⊢ HMul.hMul (β := S) s
      ((algebraMap R S : (a : R) → S)
          (x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) ⋯) :
        S) =
    HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R) : S)
have e_a : x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) sorry =
  (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)
Tactic: congr
-- 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
x : R
inst_3 : Away x S
s : S
⊢ Associated ((algebraMap R S : (a : R) → S) (sec x s).1) s
have rw : Associated (s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) (sec x s).2) s
Tactic: rw [← IsLocalization.Away.sec_spec, map_pow]
-- 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
x : R
inst_3 : Away x S
z : S
⊢ ∃ (n : ℕ) (a : R), z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
have obtain : ∀ (a : R) (n : ℕ)
  (h :
    HMul.hMul (β := S) z
        ((algebraMap R S : (a : R) → S)
            (↑(a,
                    Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                      ((fun (x_1 : ℕ) ↦ x ^ x_1) n) sorry).2 :
              R) :
          S) =
      (algebraMap R S : (a : R) → S)
        (a,
            Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
              ((fun (x_1 : ℕ) ↦ x ^ x_1) n) sorry).1),
  ∃ (n : ℕ) (a : R), z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
Tactic: obtain ⟨⟨a, ⟨-, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers x) z
-- 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
x : R
inst_3 : Away x S
z : S
a : R
n : ℕ
h :
  HMul.hMul (β := S) z
      ((algebraMap R S : (a : R) → S)
          (↑(a,
                  Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                    ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).2 :
            R) :
        S) =
    (algebraMap R S : (a : R) → S)
      (a,
          Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).1
⊢ ∃ (n : ℕ) (a : R), z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
have h₁ : z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
Tactic: use n, a
-- 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
x : R
inst_3 : Away x S
a b : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
⊢ ∃ (n : ℕ), x ^ n * a = x ^ n * b
have obtain : ∀ (n : ℕ)
  (hx :
    (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
              ((fun (x_1 : ℕ) ↦ x ^ x_1) n) sorry) :
          R) *
        a =
      (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
              ((fun (x_1 : ℕ) ↦ x ^ x_1) n) sorry) :
          R) *
        b),
  ∃ (n : ℕ), x ^ n * a = x ^ n * b
Tactic: obtain ⟨⟨-, n, rfl⟩, hx⟩ := IsLocalization.exists_of_eq (M := Submonoid.powers x) 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
x : R
inst_3 : Away x S
a b : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hx :
  (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯) :
        R) *
      a =
    (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯) :
        R) *
      b
w : ℕ
⊢ ∃ (n : ℕ), x ^ n * a = x ^ n * b
have h₁ : x ^ n * a = x ^ n * b
Tactic: use n
-- 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
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit (M := S)
    ((algebraMap R S : (a : R) → S)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x)
              ((fun (x : ℕ) ↦ r ^ x) n) ⋯) :
          R) :
      S)
have simp : IsUnit (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
Tactic: simp only [map_pow]
-- 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
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
z : S
⊢ ∃ (x : R × ↥(Submonoid.powers r)),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
have obtain : ∀ (n : ℕ) (a : R)
  (hn : z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a),
  ∃ (x : R × ↥(Submonoid.powers r)),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
Tactic: obtain ⟨n, a, hn⟩ := surj z
-- 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
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
⊢ ∃ (x : R × ↥(Submonoid.powers r)),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
have h : HMul.hMul (β := S) z
    ((algebraMap R S : (a : R) → S)
        (↑(a, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) sorry).2 :
          R) :
      S) =
  (algebraMap R S : (a : R) → S)
    (a, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) sorry).1
Tactic: use ⟨a, ⟨r ^ n, n, rfl⟩⟩
-- 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
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
x y : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
⊢ ∃ (c : ↥(Submonoid.powers r)), (↑c : R) * x = (↑c : R) * y
have obtain : ∀ (n : ℕ) (hn : r ^ n * x = r ^ n * y), ∃ (c : ↥(Submonoid.powers r)), (↑c : R) * x = (↑c : R) * y
Tactic: obtain ⟨n, hn⟩ := exists_of_eq x y 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
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
x y : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
n : ℕ
hn : r ^ n * x = r ^ n * y
⊢ ∃ (c : ↥(Submonoid.powers r)), (↑c : R) * x = (↑c : R) * y
have w : ↥(Submonoid.powers r)
Tactic: use ⟨r ^ n, n, rfl⟩
-- 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
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
x y : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
n : ℕ
hn : r ^ n * x = r ^ n * y
w : ↥(Submonoid.powers r)
⊢ ∃ (c : ↥(Submonoid.powers r)), (↑c : R) * x = (↑c : R) * y
have h₁ : (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) sorry) : R) * x =
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) sorry) : R) * y
Tactic: use ⟨r ^ n, n, rfl⟩
-- 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
r r' : R
h : Associated r r'
inst_3 : Away r S
⊢ Away r' S
have obtain : ∀ (u : Rˣ), Away (r * (↑u : R)) S
Tactic: obtain ⟨u, rfl⟩ := h
Cleared hypotheses: r', 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
r : R
inst_3 : Away r S
u : Rˣ
⊢ Away (r * (↑u : R)) S
have refine_1 : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S)
Tactic: refine mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)
-- 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
r : R
inst_3 : Away r S
u : Rˣ
refine_1 : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S)
⊢ Away (r * (↑u : R)) S
have refine_2 : ∀ (s : S),
  ∃ (n : ℕ) (a : R),
    s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a
Tactic: refine mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)
-- 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
r : R
inst_3 : Away r S
u : Rˣ
refine_1 : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S)
refine_2 :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a
⊢ Away (r * (↑u : R)) S
have refine_3 : ∀ (a b : R) (hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)),
  ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
Tactic: refine mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)
-- 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
r : R
inst_3 : Away r S
u : Rˣ
s : S
⊢ ∃ (n : ℕ) (a : R),
    s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a
have refine_2 : ∀ (n : ℕ) (a : R)
  (hn : s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a),
  ∃ (n : ℕ) (a : R),
    s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a
Tactic: obtain ⟨n, a, hn⟩ := surj r s
-- 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
r : R
inst_3 : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
⊢ ∃ (n : ℕ) (a : R),
    s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a
have h : s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n =
  (algebraMap R S : (a : R) → S) (a * (↑u : R) ^ n)
Tactic: use n, a * u ^ n
-- 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
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
⊢ ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
have refine_3 : ∀ (n : ℕ) (hn : r ^ n * a = r ^ n * b), ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
Tactic: obtain ⟨n, hn⟩ := exists_of_eq r hab
-- 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
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
have h : (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
Tactic: use n
-- 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
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
have h : r ^ n * (↑u : R) ^ n * a = r ^ n * (↑u : R) ^ n * b
Tactic: rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, 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
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hn : r ^ n * a = r ^ n * b
h : r ^ n * (↑u : R) ^ n * a = r ^ n * (↑u : R) ^ n * b
⊢ (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
have h₁ : (↑u : R) ^ n * r ^ n * a = (↑u : R) ^ n * r ^ n * b
Tactic: rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]