awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
this_1 : Module.Finite K L
this_2 : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x : L
⊢ Membership.mem (γ := IntermediateField K L) (separableClosure K L) x ↔ Membership.mem (γ := Subring L) ⊤ x
have h : Membership.mem (γ := IntermediateField K L) (separableClosure K L) x ↔
  Membership.mem (γ := Subring L)
    (RingHom.range (R := ↥(separableClosure K L)) (algebraMap (↥(separableClosure K L)) L)) x
Tactic: rw [← range_eq_top_of_isPurelyInseparable (separableClosure K L) L]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
⊢ ¬HPow.hPow (α := K[X]) (β := ℕ)
        (minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      p
have this : FiniteType K A
Tactic: have : Algebra.FiniteType K A := .of_surjective _ hp₂
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this : FiniteType K A
⊢ ¬HPow.hPow (α := K[X]) (β := ℕ)
        (minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      p
have this₁ : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
Tactic: have := Algebra.FormallyUnramified.finite_of_free K (Localization.AtPrime Q)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
⊢ ¬HPow.hPow (α := K[X]) (β := ℕ)
        (minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      p
have this₁ : IsField.{u_2} (Localization.AtPrime Q)
Tactic: have : IsField (Localization.AtPrime Q) :=
    have := IsArtinianRing.of_finite K (Localization.AtPrime Q)
    have := Algebra.FormallyUnramified.isReduced_of_field K (Localization.AtPrime Q)
    IsArtinianRing.isField_of_isReduced_of_isLocalRing _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
⊢ Eq (α := Localization.AtPrime Q)
    ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
      Localization.AtPrime Q)
    (0 : Localization.AtPrime Q)
have a : Eq (α := Q.ResidueField)
  ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField)
      ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q)) :
    Q.ResidueField)
  ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
    Q.ResidueField)
Tactic: apply (algebraMap (Localization.AtPrime Q) Q.ResidueField).injective
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
⊢ Eq (α := Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField)
        ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q)) :
      Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
have a : Eq (α := Q.ResidueField)
  ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) ((aeval x : (a : K[X]) → A) q) : Q.ResidueField)
  ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
    Q.ResidueField)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← aeval_algebraMap_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
a :
  Eq (α := Q.ResidueField)
    ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) ((aeval x : (a : K[X]) → A) q) : Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
⊢ Eq (α := Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField)
        ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q)) :
      Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
have a₁ : Eq (α := Q.ResidueField)
  (((aeval ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x) :
          AlgHom.{u_1, u_1, u_2} K K[X] Q.ResidueField) :
        (a : K[X]) → Q.ResidueField)
      q :
    Q.ResidueField)
  ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
    Q.ResidueField)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← aeval_algebraMap_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
a :
  Eq (α := Q.ResidueField)
    ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) ((aeval x : (a : K[X]) → A) q) : Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
a₁ :
  Eq (α := Q.ResidueField)
    (((aeval ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x) :
            AlgHom.{u_1, u_1, u_2} K K[X] Q.ResidueField) :
          (a : K[X]) → Q.ResidueField)
        q :
      Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
⊢ Eq (α := Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField)
        ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q)) :
      Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
have a₂ : Eq.{u_2 + 1} (α := Q.ResidueField) 0
  ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← aeval_algebraMap_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
a :
  Eq (α := Q.ResidueField)
    ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) ((aeval x : (a : K[X]) → A) q) : Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
a₁ :
  Eq (α := Q.ResidueField)
    (((aeval ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x) :
            AlgHom.{u_1, u_1, u_2} K K[X] Q.ResidueField) :
          (a : K[X]) → Q.ResidueField)
        q :
      Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
a₂ :
  Eq.{u_2 + 1} (α := Q.ResidueField) 0
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0)
⊢ Eq (α := Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField)
        ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q)) :
      Q.ResidueField)
    ((algebraMap (Localization.AtPrime Q) Q.ResidueField : (a : Localization.AtPrime Q) → Q.ResidueField) 0 :
      Q.ResidueField)
have a₃ : Eq.{u_2 + 1} (α := Q.ResidueField) 0 0
Tactic: rw [← IsScalarTower.algebraMap_apply, ← aeval_algebraMap_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p
have this₁ : Eq (α := Localization.AtPrime Q)
  ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
    Localization.AtPrime Q)
  (0 : Localization.AtPrime Q)
Tactic: have : algebraMap A (Localization.AtPrime Q) (aeval x q) = 0 := by
    apply (algebraMap (Localization.AtPrime Q) Q.ResidueField).injective
    rw [← IsScalarTower.algebraMap_apply, ← aeval_algebraMap_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this_4 : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
this :
  Eq (α := Localization.AtPrime Q)
    ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
      Localization.AtPrime Q)
    (0 : Localization.AtPrime Q)
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p
have obtain : ∀ (m : A) (hm : m ∈ Q.primeCompl)
  (hm' :
    HMul.hMul (β := A) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Q.primeCompl) m hm) : A)
        ((aeval x : (a : K[X]) → A) q : A) =
      0),
  ¬HPow.hPow (β := ℕ) q 2 ∣ p
Tactic: obtain ⟨⟨m, hm⟩, hm'⟩ := (IsLocalization.map_eq_zero_iff Q.primeCompl _ _).mp this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this_4 : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
this :
  Eq (α := Localization.AtPrime Q)
    ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
      Localization.AtPrime Q)
    (0 : Localization.AtPrime Q)
m : A
hm : m ∈ Q.primeCompl
hm' :
  HMul.hMul (β := A) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Q.primeCompl) m hm) : A) ((aeval x : (a : K[X]) → A) q : A) =
    0
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p
have obtain : ∀ (m : K[X]) (hm : Membership.mem (α := A) Q.primeCompl ((aeval x : (a : K[X]) → A) m : A))
  (hm' :
    HMul.hMul (α := A) (β := A)
        ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Q.primeCompl) ((aeval x : (a : K[X]) → A) m) hm) : A) : A)
        ((aeval x : (a : K[X]) → A) q : A) =
      0),
  ¬HPow.hPow (β := ℕ) q 2 ∣ p
Tactic: obtain ⟨m, rfl⟩ := hp₂ m
Cleared hypotheses: m, hm, hm'
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this_4 : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
this :
  Eq (α := Localization.AtPrime Q)
    ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
      Localization.AtPrime Q)
    (0 : Localization.AtPrime Q)
m : K[X]
hm : Membership.mem (α := A) Q.primeCompl ((aeval x : (a : K[X]) → A) m : A)
hm' :
  HMul.hMul (α := A) (β := A)
      ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Q.primeCompl) ((aeval x : (a : K[X]) → A) m) hm) : A) : A)
      ((aeval x : (a : K[X]) → A) q : A) =
    0
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p
have hm'₁ : p ∣ m * q
Tactic: simp_rw [← map_mul, ← AlgHom.coe_toRingHom, ← AlgHom.toRingHom_eq_coe, ← RingHom.mem_ker,
    ← hp₁, Ideal.mem_span_singleton] at hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this_4 : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
this :
  Eq (α := Localization.AtPrime Q)
    ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
      Localization.AtPrime Q)
    (0 : Localization.AtPrime Q)
m : K[X]
hm : Membership.mem (α := A) Q.primeCompl ((aeval x : (a : K[X]) → A) m : A)
hm' : p ∣ m * q
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p
have rw : ¬q * q ∣ p
Tactic: rw [pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this_4 : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
this :
  Eq (α := Localization.AtPrime Q)
    ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
      Localization.AtPrime Q)
    (0 : Localization.AtPrime Q)
m : K[X]
hm : Membership.mem (α := A) Q.primeCompl ((aeval x : (a : K[X]) → A) m : A)
hm' : p ∣ m * q
H : q * q ∣ p
⊢ False
have this₁ : q ∣ m
Tactic: have := (mul_dvd_mul_iff_right (minpoly.ne_zero (Algebra.IsIntegral.isIntegral _))).mp
    (H.trans hm')
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
Q : Ideal A
inst_3 : Q.IsPrime
inst_4 : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Eq (α := Ideal K[X]) (Ideal.span {p}) (RingHom.ker (F := RingHom.{u_1, u_2} K[X] A) (AlgHom.toRingHom (aeval x)))
hp₂ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K[X]) (β := A) (⇑(aeval x) : (a : K[X]) → A)
this_1 : FiniteType K A
this_2 : Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)
this_3 : IsField.{u_2} (Localization.AtPrime Q)
this_4 : Field (Localization.AtPrime Q) := this_3.toField
q : K[X] :=
  minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField)
this_5 :
  Eq (α := Localization.AtPrime Q)
    ((algebraMap A (Localization.AtPrime Q) : (a : A) → Localization.AtPrime Q) ((aeval x : (a : K[X]) → A) q) :
      Localization.AtPrime Q)
    (0 : Localization.AtPrime Q)
m : K[X]
hm : Membership.mem (α := A) Q.primeCompl ((aeval x : (a : K[X]) → A) m : A)
hm' : p ∣ m * q
H : q * q ∣ p
this : q ∣ m
⊢ False
have this₁ : Membership.mem (α := A) Q ((aeval x : (a : K[X]) → A) m : A)
Tactic: rw [minpoly.dvd_iff, aeval_algebraMap_apply, Q.algebraMap_residueField_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ FormallyUnramified R S ↔
    ∃ (t : S ⊗[R] S),
      (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
        Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S)
have rw : (∃ (e : S ⊗[R] S), IsIdempotentElem e ∧ Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)) ↔
  ∃ (t : S ⊗[R] S),
    (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
      Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S)
Tactic: rw [formallyUnramified_iff, KaehlerDifferential,
    Ideal.cotangent_subsingleton_iff, Ideal.isIdempotentElem_iff_of_fg _
      (KaehlerDifferential.ideal_fg R S)]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ (∃ (e : S ⊗[R] S), IsIdempotentElem e ∧ Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)) ↔
    ∃ (t : S ⊗[R] S),
      (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
        Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S)
have this : ∀ (t : S ⊗[R] S),
  Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
    Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
Tactic: have : ∀ t : S ⊗[R] S, TensorProduct.lmul' R t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S := by
    intro t
    simp only [KaehlerDifferential.ideal, RingHom.mem_ker, map_sub, map_one,
      sub_eq_zero, @eq_comm S 1]