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
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
a :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (R := Localization.AtPrime p) (F := RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
⊢ Algebra.IsSeparable.{u_1, u_2} (ResidueField (Localization.AtPrime p)) (ResidueField (Localization.AtPrime q)) ∧
      Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
        (Ideal.map (R := Localization.AtPrime p) (F :=
          RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
          (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)))
        (maximalIdeal (Localization.AtPrime q)) ↔
    Algebra.IsSeparable.{u_1, u_2} p.ResidueField q.ResidueField ∧
      Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
        (maximalIdeal (Localization.AtPrime q))

Tactic:
congr!
-- 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
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_9 : IsUnramifiedAt R q
⊢ Algebra.IsSeparable.{u_1, u_2} p.ResidueField q.ResidueField

Tactic:
((Algebra.isUnramifiedAt_iff_map_eq _ _ _).mp inferInstance).1

Premises used: inferInstance, Algebra.isUnramifiedAt_iff_map_eq, And.left, Iff.mp
-- 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
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_9 : IsUnramifiedAt R q
⊢ Module.Finite.{u_1, u_2} p.ResidueField q.ResidueField

Tactic:
Algebra.FormallyUnramified.finite_of_free _ _

Premises used: Algebra.FormallyUnramified.finite_of_free
-- 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 : Algebra.IsIntegral R S
inst_6 : FaithfulSMul R S
rw :
  ∀ (a : Localization.AtPrime p),
    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)
            a :
          Localization.AtPrime q)
        (0 : Localization.AtPrime q) →
      a = 0
⊢ 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)

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
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)
obtain :
  ∀ (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
⊢ x = 0

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x

Premises used: Ideal.primeCompl, 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
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 ∉ q, HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0

Tactic:
simpa [Localization.localRingHom_mk', IsLocalization.mk'_eq_zero_iff] using hx

Premises used: Localization.localRingHom_mk', IsLocalization.mk'_eq_zero_iff
-- 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 : 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)
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
⊢ 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

Premises used: Algebra.algebraMap, DFunLike.coe
-- 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 : 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
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
⊢ 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

Premises used: Localization.r, 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 : 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

Tactic:
(IsLocalization.mk'_eq_zero_iff _ _).mpr
    ⟨⟨r, hrp⟩, FaithfulSMul.algebraMap_injective R S ?_⟩

Premises used: Iff.mpr, Subtype.mk, FaithfulSMul.algebraMap_injective, IsLocalization.mk'_eq_zero_iff, Exists.intro
-- 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 : 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
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)
⊢ Eq (α := Localization.AtPrime p) (IsLocalization.mk' (Localization.AtPrime p) x s) 0

Tactic:
refine (IsLocalization.mk'_eq_zero_iff _ _).mpr
    ⟨⟨r, hrp⟩, FaithfulSMul.algebraMap_injective R S ?_⟩

Premises used: Iff.mpr, Subtype.mk, FaithfulSMul.algebraMap_injective, IsLocalization.mk'_eq_zero_iff, Exists.intro
-- 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 : 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.{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:
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
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)

Tactic:
obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R) (M := S)

Premises used: Module.Finite.fg_top
-- 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
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)

Tactic:
⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, Module.Finite.of_fg_top, Exists.intro, DFunLike.coe, Finset.image
-- 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
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)) ⊤
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)))
    ⊤
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
refine ⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩
-- 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
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)) ⊤
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)))
⊢ 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:
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]

Premises used: AlgHom.coe_toLinearMap, Submodule.span_span_of_tower, IsScalarTower.coe_toAlgHom', Submodule.map_top, Finset.coe_image, LinearMap.coe_range, top_le_iff, Submodule.map_span
-- 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
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
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))
⊢ 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:
obtain ⟨x, ⟨s, hsq⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x

Premises used: Ideal.primeCompl, 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
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
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))
⊢ 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

Premises used: Localization.r, 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
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
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)
⊢ 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:
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]

Premises used: mul_assoc, mul_left_comm, Submodule.smul_mem_iff_of_isUnit, Subtype.mk, map_mul, IsLocalization.map_units, IsLocalization.mk'_spec'_mk, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- 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
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 (α := 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:
Submodule.subset_span ⟨_, rfl⟩

Premises used: Set.Mem, Exists.intro, Submodule.subset_span, 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
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 (α := 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:
exact Submodule.subset_span ⟨_, 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
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)
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
have := Localization.finite_of_primesOver_eq_singleton hq