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 : Algebra.IsIntegral R S
inst_6 : FaithfulSMul R S
⊢ 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)
have rw : ∀ (a : Localization.AtPrime p),
  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)
          a :
        Localization.AtPrime q)
      (0 : Localization.AtPrime q) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
inst_6 : FaithfulSMul R S
x : Localization.AtPrime p
hx :
  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)
        x :
      Localization.AtPrime q)
    (0 : Localization.AtPrime q)
⊢ x = 0
have obtain : ∀ (x : R) (s : ↥p.primeCompl)
  (hx :
    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)
          (IsLocalization.mk' (Localization.AtPrime p) x s) :
        Localization.AtPrime q)
      (0 : Localization.AtPrime q)),
  Eq (α := Localization.AtPrime p) (IsLocalization.mk' (Localization.AtPrime p) x s) 0
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
inst_6 : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx :
  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)
        (IsLocalization.mk' (Localization.AtPrime p) x s) :
      Localization.AtPrime q)
    (0 : Localization.AtPrime q)
⊢ Eq (α := Localization.AtPrime p) (IsLocalization.mk' (Localization.AtPrime p) x s) 0
have obtain : ∀ (a : S) (haq : a ∉ q) (e : HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0),
  Eq (α := Localization.AtPrime p) (IsLocalization.mk' (Localization.AtPrime p) x s) 0
Tactic: obtain ⟨a, haq, e⟩ : ∃ a ∉ q, a * (algebraMap R S) x = 0 := by
    simpa [Localization.localRingHom_mk', IsLocalization.mk'_eq_zero_iff] using hx
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
inst_6 : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx :
  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)
        (IsLocalization.mk' (Localization.AtPrime p) x s) :
      Localization.AtPrime q)
    (0 : Localization.AtPrime q)
a : S
haq : a ∉ q
e : HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0
⊢ Eq (α := Localization.AtPrime p) (IsLocalization.mk' (Localization.AtPrime p) x s) 0
have obtain : ∀ (r : R) (hrp : r ∉ p) (t : S) (e' : (algebraMap R S : (a : R) → S) r = a * t),
  Eq (α := Localization.AtPrime p) (IsLocalization.mk' (Localization.AtPrime p) x s) 0
Tactic: obtain ⟨r, hrp, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ haq
-- 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 : Algebra.IsIntegral R S
inst_6 : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx :
  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)
        (IsLocalization.mk' (Localization.AtPrime p) x s) :
      Localization.AtPrime q)
    (0 : Localization.AtPrime q)
a : S
haq : a ∉ q
e : HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0
r : R
hrp : r ∉ p
t : S
e' : (algebraMap R S : (a : R) → S) r = a * t
⊢ Eq (α := Localization.AtPrime p) (IsLocalization.mk' (Localization.AtPrime p) x s) 0
have refine : Eq.{u_2 + 1} (α := S)
  ((algebraMap R S : (a : R) → S) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ p.primeCompl) r hrp) : R) * x) : S)
  ((algebraMap R S : (a : R) → S) 0 : S)
Tactic: refine (IsLocalization.mk'_eq_zero_iff _ _).mpr
    ⟨⟨r, hrp⟩, FaithfulSMul.algebraMap_injective R S ?_⟩
-- 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.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
have obtain : ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
  Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
Tactic: obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R) (M := S)
-- 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.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
have refine : Eq (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
  (Submodule.span (Localization.AtPrime p)
    (↑(Finset.image
          (⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Localization.AtPrime q))) :
            (a : S) → Localization.AtPrime q)
          s) :
      Set (Localization.AtPrime q)))
  ⊤
Tactic: refine ⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩
-- 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.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
⊢ Eq (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (↑(Finset.image
            (⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Localization.AtPrime q))) :
              (a : S) → Localization.AtPrime q)
            s) :
        Set (Localization.AtPrime q)))
    ⊤
have rw : LE.le (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
  (Submodule.span (Localization.AtPrime p)
    (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
Tactic: rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs,
    Submodule.map_top, LinearMap.coe_range, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom',
    ← 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.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤
x : Localization.AtPrime q
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
    x
have obtain : ∀ (x s : S) (hsq : s ∈ q.primeCompl),
  Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
    (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hsq))
Tactic: obtain ⟨x, ⟨s, hsq⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
Cleared hypotheses: 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.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
s_1 : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s_1 : Set S)) ⊤
x s : S
hsq : s ∈ q.primeCompl
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
    (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hsq))
have obtain : ∀ (r : R) (hr : r ∉ p) (t : S) (e' : (algebraMap R S : (a : R) → S) r = s * t),
  Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
    (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hsq))
Tactic: obtain ⟨r, hr, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hsq
-- 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.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
s_1 : Finset S
hs : Eq (α := Submodule R S) (Submodule.span R (↑s_1 : Set S)) ⊤
x s : S
hsq : s ∈ q.primeCompl
r : R
hr : r ∉ p
t : S
e' : (algebraMap R S : (a : R) → S) r = s * t
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
    (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hsq))
have rw : Membership.mem (α := Localization.AtPrime q) (γ :=
  Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
  (Submodule.span (Localization.AtPrime p)
    (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
  ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q) (t * x) : Localization.AtPrime q)
Tactic: rw [← Submodule.smul_mem_iff_of_isUnit _ (IsLocalization.map_units (M := p.primeCompl) _ ⟨r, hr⟩),
    Algebra.smul_def, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply _ S, e',
      map_mul, mul_assoc, mul_left_comm, IsLocalization.mk'_spec'_mk, ← map_mul]
-- 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.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
have obtain : ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
  Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
Tactic: classical
  obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R) (M := S)
  refine ⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩
  rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs,
    Submodule.map_top, LinearMap.coe_range, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom',
    ← top_le_iff]
  rintro x -
  obtain ⟨x, ⟨s, hsq⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  obtain ⟨r, hr, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hsq
  rw [← Submodule.smul_mem_iff_of_isUnit _ (IsLocalization.map_units (M := p.primeCompl) _ ⟨r, hr⟩),
    Algebra.smul_def, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply _ S, e',
      map_mul, mul_assoc, mul_left_comm, IsLocalization.mk'_spec'_mk, ← map_mul]
  exact Submodule.subset_span ⟨_, 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
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
have obtain₁ : ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
  Eq (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (↑(Finset.image
            (⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Localization.AtPrime q))) :
              (a : S) → Localization.AtPrime q)
            s) :
        Set (Localization.AtPrime q)))
    ⊤
Tactic: classical
  obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R) (M := S)
  refine ⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩
  rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs,
    Submodule.map_top, LinearMap.coe_range, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom',
    ← top_le_iff]
  rintro x -
  obtain ⟨x, ⟨s, hsq⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  obtain ⟨r, hr, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hsq
  rw [← Submodule.smul_mem_iff_of_isUnit _ (IsLocalization.map_units (M := p.primeCompl) _ ⟨r, hr⟩),
    Algebra.smul_def, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply _ S, e',
      map_mul, mul_assoc, mul_left_comm, IsLocalization.mk'_spec'_mk, ← map_mul]
  exact Submodule.subset_span ⟨_, 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
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
obtain₁ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    Eq (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Submodule.span (Localization.AtPrime p)
        (↑(Finset.image
              (⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Localization.AtPrime q))) :
                (a : S) → Localization.AtPrime q)
              s) :
          Set (Localization.AtPrime q)))
      ⊤
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
have obtain₂ : ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
  LE.le (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
    (Submodule.span (Localization.AtPrime p)
      (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
Tactic: classical
  obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R) (M := S)
  refine ⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩
  rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs,
    Submodule.map_top, LinearMap.coe_range, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom',
    ← top_le_iff]
  rintro x -
  obtain ⟨x, ⟨s, hsq⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  obtain ⟨r, hr, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hsq
  rw [← Submodule.smul_mem_iff_of_isUnit _ (IsLocalization.map_units (M := p.primeCompl) _ ⟨r, hr⟩),
    Algebra.smul_def, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply _ S, e',
      map_mul, mul_assoc, mul_left_comm, IsLocalization.mk'_spec'_mk, ← map_mul]
  exact Submodule.subset_span ⟨_, 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
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
obtain₁ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    Eq (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Submodule.span (Localization.AtPrime p)
        (↑(Finset.image
              (⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Localization.AtPrime q))) :
                (a : S) → Localization.AtPrime q)
              s) :
          Set (Localization.AtPrime q)))
      ⊤
obtain₂ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    LE.le (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
      (Submodule.span (Localization.AtPrime p)
        (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
have obtain₃ : ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤) ⦃x : Localization.AtPrime q⦄,
  Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (Submodule.span (Localization.AtPrime p)
      (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
    x
Tactic: classical
  obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R) (M := S)
  refine ⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩
  rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs,
    Submodule.map_top, LinearMap.coe_range, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom',
    ← top_le_iff]
  rintro x -
  obtain ⟨x, ⟨s, hsq⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  obtain ⟨r, hr, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hsq
  rw [← Submodule.smul_mem_iff_of_isUnit _ (IsLocalization.map_units (M := p.primeCompl) _ ⟨r, hr⟩),
    Algebra.smul_def, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply _ S, e',
      map_mul, mul_assoc, mul_left_comm, IsLocalization.mk'_spec'_mk, ← map_mul]
  exact Submodule.subset_span ⟨_, rfl⟩
-- 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)
⊢ Function.Surjective.{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)
have this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
Tactic: have := Localization.finite_of_primesOver_eq_singleton hq
-- 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)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
have rw : 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)
Tactic: rw [← Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]