awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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)
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'))
⊢ ∃ 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)

Premises used: Localization.AtPrime, IsLocalization.map_eq_zero_iff, Iff.mp, Ideal.primeCompl, Subtype.val
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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
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)
⊢ 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:
rw [← hs, Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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)

Tactic:
(IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mpr ⟨⟨_, 1, rfl⟩, ?_⟩

Premises used: Iff.mpr, Finset.univ, Set.Mem, IsLocalization.map_eq_zero_iff, setOf, Finset.prod, Subtype.mk, Set.preimage, Submonoid.powers, Set.singleton, Exists.intro, OfNat.ofNat, Subtype.val, rfl
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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)
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) ⋯) :
        R) *
      x =
    0
⊢ 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)

Tactic:
refine (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mpr ⟨⟨_, 1, rfl⟩, ?_⟩

Premises used: Iff.mpr, Finset.univ, IsLocalization.map_eq_zero_iff, Finset.prod, Subtype.mk, Submonoid.powers, Exists.intro, OfNat.ofNat, Subtype.val, rfl
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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)
simp : (↑(∏ i : ↥s, m i) : R) * x = 0
⊢ (↑(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

Tactic:
simp only [pow_one]

Premises used: pow_one
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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
rw₅ rw₆ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (↑(∏ i : ↥s, 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]

Premises used: mul_assoc, Fintype.prod_eq_mul_prod_compl, mul_left_comm, MulZeroClass.mul_zero, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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))))

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]
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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'))

Tactic:
⟨_, (∏ i : s, m i).2, ?_⟩

Premises used: Finset.univ, Finset.prod, And.intro, Exists.intro, Subtype.property
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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))))
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'))
⊢ ∃ 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:
refine ⟨_, (∏ i : s, m i).2, ?_⟩
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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
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
⊢ 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:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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))
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
⊢ x = 0

Tactic:
obtain ⟨x, _, rfl⟩ := IsLocalization.exists_mk'_eq (.powers r') x

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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))
⊢ ∃ (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

Premises used: IsLocalization.map_mk', IsLocalization.Away.map, IsLocalization.mk'_eq_zero_iff, Localization.awayMap
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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
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) ⋯) :
            S)
          ((algebraMap R S : (a : R) → S) x : S) =
        0),
    Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
⊢ Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0

Tactic:
obtain ⟨⟨_, n, rfl⟩, hn⟩ := hx

Premises used: rfl
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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.{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

Premises used: map_pow, map_mul