awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
have this : ∃ (x_1 : R × ↥p.primeCompl),
  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)
        (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))
-- 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
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), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
⊢ ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
have 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)
Tactic: obtain ⟨a, b, hbp, c, hcq, hc⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
⊢ ∃ (a : R), ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)
have 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)
Tactic: obtain ⟨d, hd, e, he⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hcq
-- 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
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)) ⊤
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have 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)
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have 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'))
Tactic: choose a b hbp e using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have obtain : ∀ (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'))
Tactic: obtain ⟨r, hrp, hr⟩ := Localization.exists_awayMap_injective_of_localRingHom_injective hRS H.1
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
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'))
have refine : ∀ (r' : R),
  r * ∏ i ∈ s, b i ∣ 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: refine ⟨r * ∏ i ∈ s, b i, mul_mem (s := p.primeCompl) hrp (prod_mem fun _ _ ↦ hbp _), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
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' : R),
    r * ∏ i ∈ s, b i ∣ r' →
      Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have refine : ∀ (r' : R) (hr' : r * ∏ i ∈ s, b i ∣ r'),
  Function.Surjective.{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 fun r' hr' ↦ ⟨hr _ (.trans ⟨_, rfl⟩ hr'), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
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' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ LE.le (α := Subalgebra R (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
    (AlgHom.range (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))))
    (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))
have rw : (↑s : Set S) ⊆
  (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
        (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
        (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
    Set S)
Tactic: rw [← Algebra.map_top, Subalgebra.map_le, ← hs, Algebra.adjoin_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
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)
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' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
x : S
hxs : x ∈ (↑s : Set S)
⊢ x ∈
    (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
          (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
          (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
      Set S)
have obtain : ∀ (r'' : R) (hr' : r' = (r * ∏ i ∈ s, b i) * r''),
  x ∈
    (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
          (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
          (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
      Set S)
Tactic: obtain ⟨r'', hr'⟩ := hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
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)
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' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ x ∈
    (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
          (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
          (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
      Set S)
have refine : Eq.{u_2 + 1} (α := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
  (((AlgHom.toRingHom (awayMapₐ (Algebra.ofId R S) r') :
          RingHom.{u_1, u_2} (Away r') (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
        (a : Away r') → Away ((Algebra.ofId R S : (a : R) → S) r'))
      (IsLocalization.mk' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
          ((fun (x : ℕ) ↦ r' ^ x) 1) sorry)) :
    Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
  (((↑(IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
          S →+* Away ((Algebra.ofId R S : (a : R) → S) r')) :
        (a : S) → Away ((Algebra.ofId R S : (a : R) → S) r'))
      x :
    Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
Tactic: refine ⟨IsLocalization.mk' (M := .powers r') _
      (r'' * r * (∏ i ∈ s.erase x, b i) * a x) ⟨_, 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
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)
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' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ Eq.{u_2 + 1} (α := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
    (((AlgHom.toRingHom (awayMapₐ (Algebra.ofId R S) r') :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((Algebra.ofId R S : (a : R) → S) r'))
        (IsLocalization.mk' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            ((fun (x : ℕ) ↦ r' ^ x) 1) ⋯)) :
      Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
    (((↑(IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
            S →+* Away ((Algebra.ofId R S : (a : R) → S) r')) :
          (a : S) → Away ((Algebra.ofId R S : (a : R) → S) r'))
        x :
      Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
have dsimp : Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
  (((IsLocalization.map (T := Submonoid.powers ((algebraMap R S : (a : R) → S) r'))
            (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) (algebraMap R S) sorry :
          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' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
          (HPow.hPow (β := ℕ) r' 1) sorry)) :
    Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
  ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
        (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
      x :
    Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
Tactic: dsimp [awayMapₐ, IsLocalization.Away.map]