awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
obtain :
  ∀ (t : S) (htQ : t ∉ Q)
    (htQ' :
      ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q')
    (ht :
      Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
        (Ideal.ResidueField
            (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
        ⊤),
    ∃ (x : S),
      Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {Q} ∧
        Function.Bijective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) (β :=
          Q.ResidueField)
          (⇑(algebraMap (Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) Q.ResidueField) :
            (a : (Ideal.under (↥R[x]) Q).ResidueField) → Q.ResidueField)
⊢ ∃ (x : S),
    Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {Q} ∧
      Function.Bijective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) (β :=
        Q.ResidueField)
        (⇑(algebraMap (Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) Q.ResidueField) :
          (a : (Ideal.under (↥R[x]) Q).ResidueField) → Q.ResidueField)

Tactic:
obtain ⟨t, htQ, htQ', ht⟩ :=
    IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top (R := R) Q

Premises used: Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ ∃ (x : S),
    Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {Q} ∧
      Function.Bijective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) (β :=
        Q.ResidueField)
        (⇑(algebraMap (Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) Q.ResidueField) :
          (a : (Ideal.under (↥R[x]) Q).ResidueField) → Q.ResidueField)

Tactic:
⟨t, ?_, RingHom.injective _, ?_⟩

Premises used: RingHom.injective, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
refine_1 : Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) {Q}
refine_2 :
  Function.Surjective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (β :=
    Q.ResidueField)
    (⇑(algebraMap (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField) :
      (a : (Ideal.under (↥R[t]) Q).ResidueField) → Q.ResidueField)
⊢ ∃ (x : S),
    Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {Q} ∧
      Function.Bijective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) (β :=
        Q.ResidueField)
        (⇑(algebraMap (Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) Q.ResidueField) :
          (a : (Ideal.under (↥R[x]) Q).ResidueField) → Q.ResidueField)

Tactic:
refine ⟨t, ?_, RingHom.injective _, ?_⟩
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
e : Membership.mem (γ := Set (Ideal S)) {Q} Q'
⊢ Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) Q'

Tactic:
⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩

Premises used: Ideal.primesOver, Set.Mem, setOf, Eq.rec, inferInstance, Ideal.LiesOver.mk, And.intro, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
e : Membership.mem (γ := Set (Ideal S)) {Q} Q'
⊢ Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) Q'

Tactic:
exact ⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
refine_1 :
  ∀ (Q' : Ideal S),
    Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) Q' →
      Q'.IsPrime → Q'.LiesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) → Membership.mem (γ := Set (Ideal S)) {Q} Q'
⊢ Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) {Q}

Tactic:
refine Set.ext fun Q' ↦ ⟨fun ⟨_, _⟩ ↦ ?_, fun e ↦ by exact ⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩⟩
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
h : Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) Q'
left : Q'.IsPrime
right : Q'.LiesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q)
refine_1 : ∀ (H : Q' ∉ {Q}), False
⊢ Membership.mem (γ := Set (Ideal S)) {Q} Q'

Tactic:
by_contra! H
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
h : Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) Q'
left : Q'.IsPrime
right : Q'.LiesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q)
H : Q' ∉ {Q}
⊢ Q'.LiesOver p

Tactic:
have : Q'.LiesOver p := .trans _ (Q.under (R[t])) _
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this_3 : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
h : Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) Q'
left : Q'.IsPrime
right : Q'.LiesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q)
H : Q' ∉ {Q}
this : Q'.LiesOver p
⊢ False

Tactic:
htQ (SetLike.le_def.mp (Q'.over_def (Q.under (R[t]))).ge
      (x := ⟨t, self_mem_adjoin_singleton _ _⟩) (htQ' Q' ⟨‹_›, ‹_›⟩ H))
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this_3 : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
h : Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) Q'
left : Q'.IsPrime
right : Q'.LiesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q)
H : Q' ∉ {Q}
this : Q'.LiesOver p
⊢ False

Tactic:
exact htQ (SetLike.le_def.mp (Q'.over_def (Q.under (R[t]))).ge
      (x := ⟨t, self_mem_adjoin_singleton _ _⟩) (htQ' Q' ⟨‹_›, ‹_›⟩ H))
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
refine_2 :
  LE.le (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    (AlgHom.range (A := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q))
      (IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField))
⊢ Function.Surjective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (β :=
    Q.ResidueField)
    (⇑(IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField) :
      (a : (Ideal.under (↥R[t]) Q).ResidueField) → Q.ResidueField)

Tactic:
rw [← AlgHom.range_eq_top, ← top_le_iff, ← ht]

Premises used: AlgHom.range_eq_top, top_le_iff
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ LE.le (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    (AlgHom.range (A := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q))
      (IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField))

Tactic:
adjoin_singleton_le ?_

Premises used: Set.Mem, Algebra.adjoin_singleton_le
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
refine_2 :
  Membership.mem (α := Q.ResidueField) (γ :=
    Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (AlgHom.range (A := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q))
      (IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField))
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
⊢ LE.le (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    (AlgHom.range (A := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q))
      (IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField))

Tactic:
refine adjoin_singleton_le ?_

Premises used: Algebra.adjoin_singleton_le
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
h :
  Eq (α := Q.ResidueField)
    ((AlgHom.toRingHom.{u_1, u_3, u_3} (R := p.ResidueField)
            (IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q))
              Q.ResidueField) :
          (a : (Ideal.under (↥R[t]) Q).ResidueField) → Q.ResidueField)
        ((algebraMap (↥R[t]) (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :
            (a : ↥R[t]) → (Ideal.under (↥R[t]) Q).ResidueField)
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[t] x) t ⋯)) :
      Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
⊢ Membership.mem (α := Q.ResidueField) (γ :=
    Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (AlgHom.range (A := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q))
      (IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField))
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)

Tactic:
use algebraMap (R[t]) _ ⟨t, self_mem_adjoin_singleton _ _⟩

Premises used: Algebra.algebraMap, Algebra.adjoin, Membership.mem, Subtype, Subtype.mk, Singleton.singleton, DFunLike.coe, Algebra.self_mem_adjoin_singleton