awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' :
  Ne (α := P.ResidueField[X]) ((derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) m : P.ResidueField[X])
    (0 : P.ResidueField[X])
this : ¬m ∣ (derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)
⊢ ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have rwa : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉
  RingHom.ker (F := S →+* Q.ResidueField) (algebraMap S Q.ResidueField)
Tactic: rwa [← Ideal.ker_algebraMap_residueField Q, RingHom.mem_ker, ← aeval_algebraMap_apply,
      ← aeval_map_algebraMap P.ResidueField, ← derivative_map, ← minpoly.dvd_iff]
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' :
  Ne (α := P.ResidueField[X]) ((derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) m : P.ResidueField[X])
    (0 : P.ResidueField[X])
this : ¬m ∣ (derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)
rwa :
  ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉
    RingHom.ker (F := S →+* Q.ResidueField) (algebraMap S Q.ResidueField)
⊢ ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have rwa₁ : ¬Eq (α := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField)
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X])) :
      Q.ResidueField)
    (0 : Q.ResidueField)
Tactic: rwa [← Ideal.ker_algebraMap_residueField Q, RingHom.mem_ker, ← aeval_algebraMap_apply,
      ← aeval_map_algebraMap P.ResidueField, ← derivative_map, ← minpoly.dvd_iff]
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' :
  Ne (α := P.ResidueField[X]) ((derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) m : P.ResidueField[X])
    (0 : P.ResidueField[X])
this : ¬m ∣ (derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)
rwa :
  ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉
    RingHom.ker (F := S →+* Q.ResidueField) (algebraMap S Q.ResidueField)
rwa₁ :
  ¬Eq (α := Q.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField)
          ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X])) :
        Q.ResidueField)
      (0 : Q.ResidueField)
⊢ ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have rwa₂ : ¬Eq.{u_3 + 1} (α := Q.ResidueField)
    (((aeval ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
            AlgHom.{u_1, u_1, u_3} R R[X] Q.ResidueField) :
          (a : R[X]) → Q.ResidueField)
        ((derivative : (a : R[X]) → R[X]) q) :
      Q.ResidueField)
    (0 : Q.ResidueField)
Tactic: rwa [← Ideal.ker_algebraMap_residueField Q, RingHom.mem_ker, ← aeval_algebraMap_apply,
      ← aeval_map_algebraMap P.ResidueField, ← derivative_map, ← minpoly.dvd_iff]
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' :
  Ne (α := P.ResidueField[X]) ((derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) m : P.ResidueField[X])
    (0 : P.ResidueField[X])
⊢ ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have inr : ¬m ∣ (derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)
Tactic: suffices ¬m ∣ derivative (q.map (algebraMap R _)) by
    rwa [← Ideal.ker_algebraMap_residueField Q, RingHom.mem_ker, ← aeval_algebraMap_apply,
      ← aeval_map_algebraMap P.ResidueField, ← derivative_map, ← minpoly.dvd_iff]
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' :
  Ne (α := P.ResidueField[X]) ((derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) m : P.ResidueField[X])
    (0 : P.ResidueField[X])
⊢ ¬m ∣ (derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)
have inr : ∀ (c : P.ResidueField[X]) (hc : Polynomial.map (algebraMap R P.ResidueField) p = m * c),
  ¬m ∣ (derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)
Tactic: obtain ⟨c, hc⟩ := hmp₁
Cleared hypotheses: hmp₁
-- 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
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      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 : p.IsPrime
Tactic: have : p.IsPrime := Ideal.IsPrime.under R Q
-- 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 : p.IsPrime
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      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₁ : IsArtinianRing (p.Fiber S)
Tactic: have : IsArtinianRing (p.Fiber S) := .of_finite p.ResidueField _
-- 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
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 : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
have obtain : ∀ (x : Q.ResidueField) (hx : Eq (α := IntermediateField.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField⟮x⟯ ⊤),
  ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
Tactic: obtain ⟨x, hx⟩ := Field.exists_primitive_element p.ResidueField Q.ResidueField
-- 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 : Q.ResidueField
hx : Eq (α := IntermediateField.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField⟮x⟯ ⊤
⊢ ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
have hx₁ : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
Tactic: rw [IntermediateField.adjoin_eq_top_iff] at hx
Cleared hypotheses: hx
-- 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
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 : Q.ResidueField
hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
⊢ ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
have pos : ∀ (hx0 : x = 0),
  ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
Tactic: by_cases hx0 : x = 0
-- 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
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 : Q.ResidueField
hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
pos :
  ∀ (hx0 : x = 0),
    ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
⊢ ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
have neg : ∀ (hx0 : ¬x = 0),
  ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
Tactic: by_cases hx0 : x = 0
-- 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
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
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      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 obtain : ∀ (x : Q.ResidueField) (hx0 : x ≠ 0)
  (hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤),
  ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      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)]
        ⊤
Tactic: obtain ⟨x, hx0, hx⟩ : ∃ x : Q.ResidueField, x ≠ 0 ∧ p.ResidueField[x] = ⊤ := by
    obtain ⟨x, hx⟩ := Field.exists_primitive_element p.ResidueField Q.ResidueField
    rw [IntermediateField.adjoin_eq_top_iff] at hx
    by_cases hx0 : x = 0
    · exact ⟨1, by simp, by simpa [p, hx0] using hx⟩
    · exact ⟨x, hx0, hx⟩
-- 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
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 : Q.ResidueField
hx0 : x ≠ 0
hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      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 obtain : ∀ (x : p.ResidueField ⊗[R] S)
  (hx0 :
    Ne.{u_3 + 1} (α := Q.ResidueField)
      (((TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) sorry :
              p.ResidueField ⊗[R] S →ₐ[p.ResidueField] 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[(((TensorProduct.lift (ofId p.ResidueField Q.ResidueField)
                  (IsScalarTower.toAlgHom R S Q.ResidueField) sorry :
                p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
              (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
            x :
          Q.ResidueField)]
      ⊤),
  ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      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)]
        ⊤
Tactic: obtain ⟨x, rfl⟩ := Ideal.Fiber.lift_residueField_surjective p _ x
Cleared hypotheses: x, hx0, hx