awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
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
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤
r : p.Fiber S
hrQ :
  r ∉
    PrimeSpectrum.asIdeal
      ((α : (a : (↑(p.primesOver S) : Type u_3)) → PrimeSpectrum (p.Fiber S))
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) Q ⋯))
hrid : IsIdempotentElem r
hr :
  ∀ (q : Ideal (p.Fiber S)),
    q.IsPrime →
      q ≠
          PrimeSpectrum.asIdeal
            ((α : (a : (↑(p.primesOver S) : Type u_3)) → PrimeSpectrum (p.Fiber S))
              (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) Q ⋯)) →
        r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
⊢ 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)]
    ⊤
have this₁ : (φ : (a : p.Fiber S) → Q.ResidueField) x =
  HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
    (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
Tactic: have : φ x = (algebraMap _ p.ResidueField s)⁻¹ • algebraMap _ _ t := by
      simpa [smul_def, ← IsScalarTower.algebraMap_apply, eq_inv_mul_iff_mul_eq₀ hsQ']
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨t, htQ, htQ', ht⟩ :=
    IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top (R := R) Q
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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)
have refine_1 : Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) {Q}
Tactic: refine ⟨t, ?_, RingHom.injective _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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}
⊢ ∃ (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)
have 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)
Tactic: refine ⟨t, ?_, RingHom.injective _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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
⊢ Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) {Q}
have 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'
Tactic: refine Set.ext fun Q' ↦ ⟨fun ⟨_, _⟩ ↦ ?_, fun e ↦ by exact ⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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)
⊢ Membership.mem (γ := Set (Ideal S)) {Q} Q'
have refine_1 : ∀ (H : Q' ∉ {Q}), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
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}
⊢ False
have this₁ : Q'.LiesOver p
Tactic: have : Q'.LiesOver p := .trans _ (Q.under (R[t])) _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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
⊢ 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)
have 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))
Tactic: rw [← AlgHom.range_eq_top, ← top_le_iff, ← ht]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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))
have 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)
Tactic: refine adjoin_singleton_le ?_
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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
⊢ 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)
have 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 sorry)) :
    Q.ResidueField)
  ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
Tactic: use algebraMap (R[t]) _ ⟨t, self_mem_adjoin_singleton _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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
⊢ 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)
have h : Eq (α := Q.ResidueField)
  ((algebraMap (↥R[t]) Q.ResidueField : (a : ↥R[t]) → Q.ResidueField)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[t] x) t sorry) :
    Q.ResidueField)
  ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
Tactic: rw [AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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)
have refine_1 : Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) {Q}
Tactic: classical
  refine ⟨t, ?_, RingHom.injective _, ?_⟩
  · refine Set.ext fun Q' ↦ ⟨fun ⟨_, _⟩ ↦ ?_, fun e ↦ by exact ⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩⟩
    by_contra! H
    have : Q'.LiesOver p := .trans _ (Q.under (R[t])) _
    exact htQ (SetLike.le_def.mp (Q'.over_def (Q.under (R[t]))).ge
      (x := ⟨t, self_mem_adjoin_singleton _ _⟩) (htQ' Q' ⟨‹_›, ‹_›⟩ H))
  · change Function.Surjective (IsScalarTower.toAlgHom p.ResidueField _ _)
    rw [← AlgHom.range_eq_top, ← top_le_iff, ← ht]
    refine adjoin_singleton_le ?_
    use algebraMap (R[t]) _ ⟨t, self_mem_adjoin_singleton _ _⟩
    rw [AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom, ← IsScalarTower.algebraMap_apply]
    rfl