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
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :
      (a : Localization.AtPrime p) → Localization.AtPrime q)
have change : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
  (⇑(Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) :
    (a : Localization.AtPrime p) → Localization.AtPrime q)
Tactic: change Function.Surjective (Algebra.linearMap _ _)
-- 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
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) :
      (a : Localization.AtPrime p) → Localization.AtPrime q)
have rw : LE.le.{u_2} (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
  (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)))
Tactic: rw [← LinearMap.range_eq_top, ← top_le_iff]
-- 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
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
⊢ LE.le.{u_2} (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)))
have apply : ⊤ ≤
  LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
    HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal (Localization.AtPrime p)) (β :=
      Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) ⊤
Tactic: apply Submodule.le_of_le_smul_of_le_jacobson_bot Module.Finite.fg_top (maximalIdeal_le_jacobson _)
-- 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
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
⊢ ⊤ ≤
    LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal (Localization.AtPrime p)) (β :=
        Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p))
        ⊤
have rw : LE.le.{u_2} (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
  (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
    Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
Tactic: rw [Ideal.smul_top_eq_map, Algebra.FormallyUnramified.map_maximalIdeal]
-- 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
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x
have obtain : ∀ (a : p.ResidueField)
  (ha :
    Eq.{u_2 + 1} (α := q.ResidueField)
      ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField) a : q.ResidueField)
      ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
        q.ResidueField)),
  Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x
Tactic: obtain ⟨a, ha⟩ := H (algebraMap _ _ x)
-- 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
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : p.ResidueField
ha :
  Eq.{u_2 + 1} (α := q.ResidueField)
    ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField) a : q.ResidueField)
    ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
      q.ResidueField)
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x
have obtain : ∀ (a : Localization.AtPrime p)
  (ha :
    Eq.{u_2 + 1} (α := q.ResidueField)
      ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
          ((residue (Localization.AtPrime p) : (a : Localization.AtPrime p) → ResidueField (Localization.AtPrime p))
            a) :
        q.ResidueField)
      ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
        q.ResidueField)),
  Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x
Tactic: obtain ⟨a, rfl⟩ := residue_surjective a
Cleared hypotheses: a, ha
-- 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
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  Eq.{u_2 + 1} (α := q.ResidueField)
    ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
        ((residue (Localization.AtPrime p) : (a : Localization.AtPrime p) → ResidueField (Localization.AtPrime p)) a) :
      q.ResidueField)
    ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
      q.ResidueField)
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x
have ha₁ : Membership.mem (γ := Ideal (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime q))
  (HSub.hSub (α := Localization.AtPrime q)
    ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
          (a : Localization.AtPrime p) → Localization.AtPrime q)
        a :
      Localization.AtPrime q)
    x)
Tactic: rw [← ResidueField.algebraMap_eq, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply _ (Localization.AtPrime q), ResidueField.algebraMap_eq,
    ← sub_eq_zero, ← map_sub, residue_eq_zero_iff] at ha
Cleared hypotheses: ha
-- 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
inst_7 : Algebra.IsUnramifiedAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  Membership.mem (γ := Ideal (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime q))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      x)
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x
have rw : Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
  (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
    Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
  (HSub.hSub (α := Localization.AtPrime q)
    ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
          (a : Localization.AtPrime p) → Localization.AtPrime q)
        a :
      Localization.AtPrime q)
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      x))
Tactic: rw [← sub_sub_self (algebraMap _ _ a) x]
-- 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: obtain ⟨s, hs⟩ := hRS
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
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))
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)
have a : Eq.{u_2 + 1} (α := Localization.AtPrime q)
  (((localRingHom p q (algebraMap R S) sorry : RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) :
        (a : Localization.AtPrime p) → Localization.AtPrime q)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R)) :
    Localization.AtPrime q)
  (((localRingHom p q (algebraMap R S) sorry : RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) :
        (a : Localization.AtPrime p) → Localization.AtPrime q)
      0 :
    Localization.AtPrime q)
Tactic: apply H
-- 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))
⊢ ∃ 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 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)
Tactic: 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)]
-- 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)
⊢ ∃ 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 choose : ∀ (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'))
Tactic: choose m hm using fun x ↦ (IsLocalization.map_eq_zero_iff p.primeCompl _ _).mp (this x)
-- 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
⊢ 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))))
have rw : (↑s : Set R) ⊆
  (↑(RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
        (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))) :
    Set R)
Tactic: rw [← hs, Ideal.span_le]
-- 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)
⊢ x ∈
    (↑(RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))) :
      Set R)
have refine : (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑(∏ i : ↥s, m i) : R)) x)
          ((fun (x : ℕ) ↦ HPow.hPow (α := R) (↑(∏ i : ↥s, m i) : R) x) 1) sorry) :
      R) *
    x =
  0
Tactic: refine (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mpr ⟨⟨_, 1, 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 :
  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)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑(∏ i : ↥s, m i) : R)) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := R) (↑(∏ i : ↥s, m i) : R) x) 1) ⋯) :
        R) *
      x =
    0
have simp : (↑(∏ i : ↥s, m i) : R) * x = 0
Tactic: simp only [pow_one]
-- 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)
⊢ (↑(∏ i : ↥s, m i) : R) * x = 0
have 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
Tactic: rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      mul_zero]