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_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)
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) ⋯) :
            R) *
          (r' ^ n * x) =
        0),
    Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 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)

Premises used: Finset.univ, IsLocalization.map_eq_zero_iff, Finset.prod, Submonoid.powers, Iff.mp, 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_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

Tactic:
(IsLocalization.mk'_eq_zero_iff _ _).mpr ⟨⟨_, k + n, rfl⟩, ?_⟩

Premises used: Iff.mpr, Subtype.mk, HAdd.hAdd, IsLocalization.mk'_eq_zero_iff, Exists.intro, 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 : 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
refine :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            ((fun (x : ℕ) ↦ r' ^ x) (k + n)) ⋯) :
        R) *
      x =
    0
⊢ Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0

Tactic:
refine (IsLocalization.mk'_eq_zero_iff _ _).mpr ⟨⟨_, k + n, 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 : 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
dsimp : r' ^ (k + 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

Tactic:
dsimp only at hk ⊢
-- 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 : 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
rw₈ rw₉ : Eq.{u_1 + 1} (α := R) 0 0
⊢ r' ^ (k + n) * x = 0

Tactic:
rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]

Premises used: mul_assoc, pow_add, mul_left_comm, MulZeroClass.mul_zero, mul_pow
-- 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
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)
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'))
⊢ ∃ 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)

Premises used: Algebra.FiniteType.out
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
x : S
⊢ ∃ (x_1 : R × ↥p.primeCompl),
    Eq.{u_2 + 1} (α := Localization.AtPrime q)
      (((localRingHom p q (algebraMap R S) ⋯ : RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x_1 with
          | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m) :
        Localization.AtPrime q)
      ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q) x : Localization.AtPrime q)

Tactic:
have := (IsLocalization.mk'_surjective p.primeCompl).exists.mp (H.2 (algebraMap _ _ x))
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
x : S
this :
  ∃ (x_1 : R × ↥p.primeCompl),
    Eq.{u_2 + 1} (α := Localization.AtPrime q)
      (((localRingHom p q (algebraMap R S) ⋯ : RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x_1 with
          | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m) :
        Localization.AtPrime q)
      ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q) x : Localization.AtPrime q)
⊢ ∃ (a : R),
    ∃ a_1 ∉ p,
      ∃ a_2 ∉ q,
        HMul.hMul (β := S) a_2 ((algebraMap R S : (a : R) → S) a : S) =
          a_2 * HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) a_1 : S)

Tactic:
simp only [localRingHom_mk', Prod.exists, Subtype.exists, Ideal.mem_primeCompl_iff,
      IsLocalization.mk'_eq_iff_eq_mul, exists_prop, ← map_mul,
      IsLocalization.eq_iff_exists q.primeCompl] at this

Premises used: Localization.localRingHom_mk', Subtype.exists, exists_prop, IsLocalization.mk'_eq_iff_eq_mul, map_mul, Ideal.mem_primeCompl_iff, Ideal.primeCompl, Prod.exists, IsLocalization.eq_iff_exists
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
x : S
this :
  ∃ (a : R),
    ∃ a_1 ∉ p,
      ∃ a_2 ∉ q,
        HMul.hMul (β := S) a_2 ((algebraMap R S : (a : R) → S) a : S) =
          a_2 * HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) a_1 : S)
obtain :
  ∀ (a b : R) (hbp : b ∉ p) (c : S) (hcq : c ∉ q)
    (hc :
      HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) a : S) =
        c * HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)),
    ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
⊢ ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)

Tactic:
obtain ⟨a, b, hbp, c, hcq, hc⟩ := this
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
x : S
a b : R
hbp : b ∉ p
c : S
hcq : c ∉ q
hc :
  HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) a : S) =
    c * HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
obtain :
  ∀ (d : R) (hd : d ∉ p) (e : S) (he : (algebraMap R S : (a : R) → S) d = c * e),
    ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
⊢ ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)

Tactic:
obtain ⟨d, hd, e, he⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hcq

Premises used: Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
x : S
a b : R
hbp : b ∉ p
c : S
hcq : c ∉ q
hc :
  HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) a : S) =
    c * HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
d : R
hd : d ∉ p
e : S
he : (algebraMap R S : (a : R) → S) d = c * e
⊢ (algebraMap R S : (a : R) → S) (d * a) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (d * b) : S)

Tactic:
grind
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
x : S
a b : R
hbp : b ∉ p
c : S
hcq : c ∉ q
hc :
  HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) a : S) =
    c * HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
d : R
hd : d ∉ p
e : S
he : (algebraMap R S : (a : R) → S) d = c * e
⊢ ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)

Tactic:
exact ⟨d * a, d * b, ‹p.IsPrime›.mul_notMem hd hbp, by grind⟩
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
⊢ ∀ (x : S),
    ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)

Tactic:
have (x : S) : ∃ a, ∃ b ∉ p, algebraMap R S a = x * algebraMap R S b := by
    have := (IsLocalization.mk'_surjective p.primeCompl).exists.mp (H.2 (algebraMap _ _ x))
    simp only [localRingHom_mk', Prod.exists, Subtype.exists, Ideal.mem_primeCompl_iff,
      IsLocalization.mk'_eq_iff_eq_mul, exists_prop, ← map_mul,
      IsLocalization.eq_iff_exists q.primeCompl] at this
    obtain ⟨a, b, hbp, c, hcq, hc⟩ := this
    obtain ⟨d, hd, e, he⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hcq
    exact ⟨d * a, d * b, ‹p.IsPrime›.mul_notMem hd hbp, by grind⟩
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
this :
  ∀ (x : S),
    ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
choose :
  ∀ (a b : (x : S) → R) (hbp : ∀ (x : S), b x ∉ p)
    (e :
      ∀ (x : S),
        (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : 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'))
⊢ ∃ 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:
choose a b hbp e using this
-- 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
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)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
obtain :
  ∀ (r : R) (hrp : r ∉ p)
    (hr :
      ∀ (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.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'))
⊢ ∃ 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 ⟨r, hrp, hr⟩ := Localization.exists_awayMap_injective_of_localRingHom_injective hRS H.1

Premises used: Localization.r, Localization.exists_awayMap_injective_of_localRingHom_injective, And.left