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 :
  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 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s),
    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) → ↥p.primeCompl
hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0
x : R
hxs : x ∈ (↑s : Set R)
rw :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs) * ∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
⊢ (↑(∏ i : ↥s, m i) : R) * x = 0
have rw₁ : (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
      (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
    x =
  0
Tactic: rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      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 :
  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 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s),
    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) → ↥p.primeCompl
hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0
x : R
hxs : x ∈ (↑s : Set R)
rw :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs) * ∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
rw₁ :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
        (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
⊢ (↑(∏ i : ↥s, m i) : R) * x = 0
have rw₂ : (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
    ((↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) * x) =
  0
Tactic: rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      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 :
  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 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s),
    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) → ↥p.primeCompl
hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0
x : R
hxs : x ∈ (↑s : Set R)
rw :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs) * ∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
rw₁ :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
        (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
rw₂ :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
      ((↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) * x) =
    0
⊢ (↑(∏ i : ↥s, m i) : R) * x = 0
have rw₃ : (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
    ((↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) * x) =
  0
Tactic: rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      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 :
  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 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s),
    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) → ↥p.primeCompl
hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0
x : R
hxs : x ∈ (↑s : Set R)
rw :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs) * ∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
rw₁ :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
        (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
rw₂ :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
      ((↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) * x) =
    0
rw₃ :
  (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      ((↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) * x) =
    0
⊢ (↑(∏ i : ↥s, m i) : R) * x = 0
have rw₄ : HMul.hMul (α := R) (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) 0 = 0
Tactic: rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      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 :
  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 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s),
    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) → ↥p.primeCompl
hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0
x : R
hxs : x ∈ (↑s : Set R)
rw :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs) * ∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
rw₁ :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
        (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      x =
    0
rw₂ :
  (↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) *
      ((↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) * x) =
    0
rw₃ :
  (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) *
      ((↑(m (Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs)) : R) * x) =
    0
rw₄ : HMul.hMul (α := R) (↑(∏ i ∈ {Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hxs}ᶜ, m i) : R) 0 = 0
⊢ (↑(∏ i : ↥s, m i) : R) * x = 0
have rw₅ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (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
q : Ideal S
inst_4 : q.IsPrime
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)
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s),
    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) → ↥p.primeCompl
hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0
⊢ ∃ 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 H₁ : LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
  (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R)) (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R))))
Tactic: 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]
-- 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 : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
this :
  ∀ (x : ↥s),
    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) → ↥p.primeCompl
hm : ∀ (x : ↥s), (↑(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, m i) : R))
      (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R))))
⊢ ∃ 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 refine : ∀ (r' : R),
  (↑(∏ i : ↥s, m i) : 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: refine ⟨_, (∏ i : s, m i).2, ?_⟩
-- 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
⊢ 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 rw : ∀ (a : Away r'),
  Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (((awayMap (algebraMap R S) r' :
              RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
            (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
          a :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (0 : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) →
    a = 0
Tactic: rw [injective_iff_map_eq_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 : Away r'
hx :
  Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (((awayMap (algebraMap R S) r' :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
        x :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (0 : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
⊢ x = 0
have obtain : ∀ (x : R) (w : ↥(Submonoid.powers r'))
  (hx :
    Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (((awayMap (algebraMap R S) r' :
              RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
            (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
          (IsLocalization.mk' (Away r') x w) :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (0 : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))),
  Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
Tactic: obtain ⟨x, _, rfl⟩ := IsLocalization.exists_mk'_eq (.powers r') x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (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
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')
hx :
  Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (((awayMap (algebraMap R S) r' :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
        (IsLocalization.mk' (Away r') x w) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (0 : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
⊢ Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
have hx₁ : ∃ (m : ↥(Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S)),
  HMul.hMul (β := S) (↑m : S) ((algebraMap R S : (a : R) → S) x : S) = 0
Tactic: simp only [awayMap, IsLocalization.Away.map, IsLocalization.map_mk',
    IsLocalization.mk'_eq_zero_iff] at hx
Cleared hypotheses: hx
-- 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')
hx :
  ∃ (m : ↥(Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S)),
    HMul.hMul (β := S) (↑m : S) ((algebraMap R S : (a : R) → S) x : S) = 0
⊢ Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
have obtain : ∀ (n : ℕ)
  (hn :
    HMul.hMul (β := S)
        (↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r' : S) x) n) sorry) :
          S)
        ((algebraMap R S : (a : R) → S) x : S) =
      0),
  Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
Tactic: obtain ⟨⟨_, n, rfl⟩, hn⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (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
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 :
  HMul.hMul (β := S)
      (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r' : S) x) n) ⋯) :
        S)
      ((algebraMap R S : (a : R) → S) x : S) =
    0
⊢ Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
have hn₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)
Tactic: simp only [← map_pow, ← map_mul] at hn
Cleared hypotheses: hn
-- 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)
⊢ Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
have obtain : ∀ (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) sorry) :
          R) *
        (r' ^ n * x) =
      0),
  Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
Tactic: obtain ⟨⟨_, k, rfl⟩, hk⟩ := (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mp (H hn)