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
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)
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)
⊢ 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)

Tactic:
rw [← Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]

Premises used: Localization.AtPrime.IsLiesOverAlgebra.algebraMap_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.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)
change :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) :
      (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ 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:
change Function.Surjective (Algebra.linearMap _ _)

Premises used: Algebra.linearMap, DFunLike.coe, Function.Surjective
-- 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)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
rw :
  LE.le.{u_2} (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)))
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) :
      (a : Localization.AtPrime p) → Localization.AtPrime q)

Tactic:
rw [← LinearMap.range_eq_top, ← top_le_iff]

Premises used: LinearMap.range_eq_top, top_le_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 : 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)
apply :
  ⊤ ≤
    LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal (Localization.AtPrime p)) (β :=
        Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p))
        ⊤
⊢ LE.le.{u_2} (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)))

Tactic:
apply Submodule.le_of_le_smul_of_le_jacobson_bot Module.Finite.fg_top (maximalIdeal_le_jacobson _)

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot, Module.Finite.fg_top, IsLocalRing.maximalIdeal_le_jacobson
-- 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)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
rw :
  LE.le.{u_2} (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
⊢ ⊤ ≤
    LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal (Localization.AtPrime p)) (β :=
        Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p))
        ⊤

Tactic:
rw [Ideal.smul_top_eq_map, Algebra.FormallyUnramified.map_maximalIdeal]

Premises used: Ideal.smul_top_eq_map, Algebra.FormallyUnramified.map_maximalIdeal
-- 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)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
obtain :
  ∀ (a : p.ResidueField)
    (ha :
      Eq.{u_2 + 1} (α := q.ResidueField)
        ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField) a : q.ResidueField)
        ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
          q.ResidueField)),
    Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
        Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
      x
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x

Tactic:
obtain ⟨a, ha⟩ := H (algebraMap _ _ x)

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 : 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)
x : Localization.AtPrime q
a : p.ResidueField
ha :
  Eq.{u_2 + 1} (α := q.ResidueField)
    ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField) a : q.ResidueField)
    ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
      q.ResidueField)
obtain :
  ∀ (a : Localization.AtPrime p)
    (ha :
      Eq.{u_2 + 1} (α := q.ResidueField)
        ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
            ((residue (Localization.AtPrime p) : (a : Localization.AtPrime p) → ResidueField (Localization.AtPrime p))
              a) :
          q.ResidueField)
        ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
          q.ResidueField)),
    Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
        Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
      x
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x

Tactic:
obtain ⟨a, rfl⟩ := residue_surjective a

Premises used: rfl, IsLocalRing.residue_surjective
-- 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)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  Eq.{u_2 + 1} (α := q.ResidueField)
    ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
        ((residue (Localization.AtPrime p) : (a : Localization.AtPrime p) → ResidueField (Localization.AtPrime p)) a) :
      q.ResidueField)
    ((algebraMap (Localization.AtPrime q) q.ResidueField : (a : Localization.AtPrime q) → q.ResidueField) x :
      q.ResidueField)
⊢ Membership.mem (γ := Ideal (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime q))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      x)

Tactic:
rw [← ResidueField.algebraMap_eq, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply _ (Localization.AtPrime q), ResidueField.algebraMap_eq,
    ← sub_eq_zero, ← map_sub, residue_eq_zero_iff] at ha

Premises used: map_sub, IsLocalRing.residue_eq_zero_iff, sub_eq_zero, Localization.AtPrime, IsLocalRing.ResidueField.algebraMap_eq, 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.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)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  Membership.mem (γ := Ideal (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime q))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      x)
rw :
  Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      (HSub.hSub (α := Localization.AtPrime q)
        ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
              (a : Localization.AtPrime p) → Localization.AtPrime q)
            a :
          Localization.AtPrime q)
        x))
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    x

Tactic:
rw [← sub_sub_self (algebraMap _ _ a) x]

Premises used: Algebra.algebraMap, DFunLike.coe, sub_sub_self
-- 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)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  Membership.mem (γ := Ideal (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime q))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      x)
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      (HSub.hSub (α := Localization.AtPrime q)
        ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
              (a : Localization.AtPrime p) → Localization.AtPrime q)
            a :
          Localization.AtPrime q)
        x))

Tactic:
sub_mem (Submodule.mem_sup_left ⟨_, rfl⟩) (Submodule.mem_sup_right ha)

Premises used: Set.Mem, sub_mem, Exists.intro, Submodule.mem_sup_left, Submodule.mem_sup_right, 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)
this : Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  Membership.mem (γ := Ideal (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime q))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      x)
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
    (LinearMap.range (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)) ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q)))
    (HSub.hSub (α := Localization.AtPrime q)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
            (a : Localization.AtPrime p) → Localization.AtPrime q)
          a :
        Localization.AtPrime q)
      (HSub.hSub (α := Localization.AtPrime q)
        ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q) :
              (a : Localization.AtPrime p) → Localization.AtPrime q)
            a :
          Localization.AtPrime q)
        x))

Tactic:
refine sub_mem (Submodule.mem_sup_left ⟨_, rfl⟩) (Submodule.mem_sup_right ha)
-- 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
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
inst_5 : q.LiesOver p
H :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
obtain :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))),
    ∃ r ∉ p,
      ∀ (r' : R),
        r ∣ r' →
          Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))

Tactic:
obtain ⟨s, hs⟩ := hRS
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
x : ↥s
a :
  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)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R)) :
      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)
        0 :
      Localization.AtPrime q)
⊢ Eq (α := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
    (0 : Localization.AtPrime p)

Tactic:
apply H
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
H :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
x : ↥s
⊢ 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)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R)) :
      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)
        0 :
      Localization.AtPrime q)

Tactic:
simp [localRingHom_to_map, -FaithfulSMul.algebraMap_eq_zero_iff,
      show algebraMap R S _ = 0 from hs.le (Ideal.subset_span x.2)]

Premises used: Ideal.subset_span, Localization.localRingHom_to_map, Eq.le, Subtype.property, FaithfulSMul.algebraMap_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
inst_5 : q.LiesOver p
H :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))
⊢ ∀ (x : ↥s),
    Eq (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
      (0 : Localization.AtPrime p)

Tactic:
have (x : s) : algebraMap R (Localization.AtPrime p) x.1 = 0 := by
    apply H
    simp [localRingHom_to_map, -FaithfulSMul.algebraMap_eq_zero_iff,
      show algebraMap R S _ = 0 from hs.le (Ideal.subset_span x.2)]