awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑(∏ i : ↥s_1, m i) : R)) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) x) k) ⋯) :
        R) *
      (r' ^ n * x) =
    0
⊢ Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
have refine : (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
          ((fun (x : ℕ) ↦ r' ^ x) (k + n)) sorry) :
      R) *
    x =
  0
Tactic: refine (IsLocalization.mk'_eq_zero_iff _ _).mpr ⟨⟨_, k + n, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑(∏ i : ↥s_1, m i) : R)) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) x) k) ⋯) :
        R) *
      (r' ^ n * x) =
    0
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            ((fun (x : ℕ) ↦ r' ^ x) (k + n)) ⋯) :
        R) *
      x =
    0
have dsimp : r' ^ (k + n) * x = 0
Tactic: dsimp only at hk ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
⊢ r' ^ (k + n) * x = 0
have rw : r' ^ k * r' ^ n * x = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
⊢ r' ^ (k + n) * x = 0
have rw₁ : r' ^ k * (r' ^ n * x) = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
rw₁ : r' ^ k * (r' ^ n * x) = 0
⊢ r' ^ (k + n) * x = 0
have rw₂ : ((↑(∏ i : ↥s_1, m i) : R) * s) ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
rw₁ : r' ^ k * (r' ^ n * x) = 0
rw₂ : ((↑(∏ i : ↥s_1, m i) : R) * s) ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
⊢ r' ^ (k + n) * x = 0
have rw₃ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
rw₁ : r' ^ k * (r' ^ n * x) = 0
rw₂ : ((↑(∏ i : ↥s_1, m i) : R) * s) ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₃ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
⊢ r' ^ (k + n) * x = 0
have rw₄ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (r' ^ n * x) = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
rw₁ : r' ^ k * (r' ^ n * x) = 0
rw₂ : ((↑(∏ i : ↥s_1, m i) : R) * s) ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₃ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₄ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (r' ^ n * x) = 0
⊢ r' ^ (k + n) * x = 0
have rw₅ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (s ^ k * (r' ^ n * x)) = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
rw₁ : r' ^ k * (r' ^ n * x) = 0
rw₂ : ((↑(∏ i : ↥s_1, m i) : R) * s) ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₃ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₄ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (r' ^ n * x) = 0
rw₅ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (s ^ k * (r' ^ n * x)) = 0
⊢ r' ^ (k + n) * x = 0
have rw₆ : s ^ k * (HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x)) = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
rw₁ : r' ^ k * (r' ^ n * x) = 0
rw₂ : ((↑(∏ i : ↥s_1, m i) : R) * s) ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₃ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₄ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (r' ^ n * x) = 0
rw₅ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (s ^ k * (r' ^ n * x)) = 0
rw₆ : s ^ k * (HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x)) = 0
⊢ r' ^ (k + n) * x = 0
have rw₇ : s ^ k * 0 = 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H_1 :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s_1 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s_1),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)
m : (x : ↥s_1) → ↥p.primeCompl
hm : ∀ (x : ↥s_1), (↑(m x) : R) * (↑x : R) = 0
H :
  LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
    (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s_1, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s_1, m i) : R))))
r' s : R
e : r' = (↑(∏ i : ↥s_1, m i) : R) * s
x : R
w : ↥(Submonoid.powers r')
n : ℕ
hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
k : ℕ
hk : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x) = 0
rw : r' ^ k * r' ^ n * x = 0
rw₁ : r' ^ k * (r' ^ n * x) = 0
rw₂ : ((↑(∏ i : ↥s_1, m i) : R) * s) ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₃ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (((↑(∏ i : ↥s_1, m i) : R) * s) ^ n * x) = 0
rw₄ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * s ^ k * (r' ^ n * x) = 0
rw₅ : HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (s ^ k * (r' ^ n * x)) = 0
rw₆ : s ^ k * (HPow.hPow (α := R) (↑(∏ i : ↥s_1, m i) : R) k * (r' ^ n * x)) = 0
rw₇ : s ^ k * 0 = 0
⊢ r' ^ (k + n) * x = 0
have rw₈ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
inst_5 : q.LiesOver p
H :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have obtain : ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))),
  ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
Tactic: classical
  obtain ⟨s, hs⟩ := hRS
  have (x : s) : algebraMap R (Localization.AtPrime p) x.1 = 0 := by
    apply H
    simp [localRingHom_to_map, -FaithfulSMul.algebraMap_eq_zero_iff,
      show algebraMap R S _ = 0 from hs.le (Ideal.subset_span x.2)]
  choose m hm using fun x ↦ (IsLocalization.map_eq_zero_iff p.primeCompl _ _).mp (this x)
  have H : RingHom.ker (algebraMap R S) ≤ RingHom.ker
      (algebraMap R (Localization.Away (∏ i, m i).1)) := by
    rw [← hs, Ideal.span_le]
    intro x hxs
    refine (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mpr ⟨⟨_, 1, rfl⟩, ?_⟩
    simp only [pow_one]
    rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      mul_zero]
  refine ⟨_, (∏ i : s, m i).2, ?_⟩
  rintro r' ⟨s, e⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  obtain ⟨x, _, rfl⟩ := IsLocalization.exists_mk'_eq (.powers r') x
  simp only [awayMap, IsLocalization.Away.map, IsLocalization.map_mk',
    IsLocalization.mk'_eq_zero_iff] at hx
  obtain ⟨⟨_, n, rfl⟩, hn⟩ := hx
  simp only [← map_pow, ← map_mul] at hn
  obtain ⟨⟨_, k, rfl⟩, hk⟩ := (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mp (H hn)
  refine (IsLocalization.mk'_eq_zero_iff _ _).mpr ⟨⟨_, k + n, rfl⟩, ?_⟩
  dsimp only at hk ⊢
  rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]
Cleared hypotheses: hRS
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have obtain : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤),
  ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
Tactic: obtain ⟨s, hs⟩ := Algebra.FiniteType.out (R := R) (A := S)