awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Field
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 : FormallyUnramified (↥(separableClosure K L)) L
⊢ EssFiniteType (↥(separableClosure K L)) L

Tactic:
have := EssFiniteType.of_comp K (separableClosure K L) L
-- Module: Mathlib.RingTheory.Unramified.Field
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
h :
  ∀ (x : L),
    Membership.mem (γ := IntermediateField K L) (separableClosure K L) x ↔
      Membership.mem (γ := IntermediateField K L) ⊤ x
⊢ Eq (α := IntermediateField K L) (separableClosure K L) ⊤

Tactic:
ext
-- Module: Mathlib.RingTheory.Unramified.Field
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
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
⊢ Membership.mem (γ := IntermediateField K L) (separableClosure K L) x ↔ Membership.mem (γ := Subring L) ⊤ x

Tactic:
rw [← range_eq_top_of_isPurelyInseparable (separableClosure K L) L]

Premises used: Membership.mem, Subtype, Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable, separableClosure
-- Module: Mathlib.RingTheory.Unramified.Field
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)
      (RingHom.range (R := ↥(separableClosure K L)) (algebraMap (↥(separableClosure K L)) L)) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
inst : Field K
L : Type u
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : EssFiniteType K L
⊢ FormallyUnramified K L ↔ Algebra.IsSeparable K L

Tactic:
⟨fun _ ↦ isSeparable K L, fun _ ↦ of_isSeparable K L⟩

Premises used: Algebra.FormallyUnramified.of_isSeparable, Algebra.FormallyUnramified.isSeparable, Iff.intro
-- Module: Mathlib.RingTheory.Unramified.Field
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)
⊢ FiniteType K A

Tactic:
have : Algebra.FiniteType K A := .of_surjective _ hp₂
-- Module: Mathlib.RingTheory.Unramified.Field
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
⊢ Module.Finite.{u_1, u_2} K (Localization.AtPrime Q)

Tactic:
have := Algebra.FormallyUnramified.finite_of_free K (Localization.AtPrime Q)
-- Module: Mathlib.RingTheory.Unramified.Field
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)
⊢ 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 _
-- Module: Mathlib.RingTheory.Unramified.Field
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
set :
  let q : K[X] :=
    minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField);
  ¬HPow.hPow (β := ℕ) q 2 ∣ p
⊢ ¬HPow.hPow (α := K[X]) (β := ℕ)
        (minpoly K (B := Q.ResidueField) ((algebraMap A Q.ResidueField : (a : A) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      p

Tactic:
set q := minpoly K (algebraMap A Q.ResidueField x)

Premises used: Algebra.algebraMap, Ideal.ResidueField, minpoly, DFunLike.coe
-- Module: Mathlib.RingTheory.Unramified.Field
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 (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)
⊢ 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:
apply (algebraMap (Localization.AtPrime Q) Q.ResidueField).injective

Premises used: Algebra.algebraMap, Localization.AtPrime, Ideal.ResidueField, RingHom.injective
-- Module: Mathlib.RingTheory.Unramified.Field
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)
a₃ a₄ : Eq.{u_2 + 1} (α := Q.ResidueField) 0 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)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ← aeval_algebraMap_apply, minpoly.aeval, map_zero]

Premises used: map_zero, minpoly.aeval, IsScalarTower.algebraMap_apply, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Unramified.Field
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)

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]
-- Module: Mathlib.RingTheory.Unramified.Field
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)
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
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p

Tactic:
obtain ⟨⟨m, hm⟩, hm'⟩ := (IsLocalization.map_eq_zero_iff Q.primeCompl _ _).mp this

Premises used: IsLocalization.map_eq_zero_iff, Iff.mp, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Unramified.Field
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
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
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p

Tactic:
obtain ⟨m, rfl⟩ := hp₂ m

Premises used: rfl
-- Module: Mathlib.RingTheory.Unramified.Field
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
⊢ 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'

Premises used: AlgHom.coe_toRingHom, RingHom.mem_ker, map_mul, AlgHom.toRingHom_eq_coe, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Unramified.Field
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
rw : ¬q * q ∣ p
⊢ ¬HPow.hPow (β := ℕ) q 2 ∣ p

Tactic:
rw [pow_two]

Premises used: pow_two
-- Module: Mathlib.RingTheory.Unramified.Field
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
⊢ q ∣ m

Tactic:
have := (mul_dvd_mul_iff_right (minpoly.ne_zero (Algebra.IsIntegral.isIntegral _))).mp
    (H.trans hm')
-- Module: Mathlib.RingTheory.Unramified.Field
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
⊢ 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

Premises used: minpoly.dvd_iff, Ideal.algebraMap_residueField_eq_zero, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Unramified.Field
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 : Membership.mem (α := A) Q ((aeval x : (a : K[X]) → A) m : A)
⊢ False

Tactic:
hm this
-- Module: Mathlib.RingTheory.Unramified.Field
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 : Membership.mem (α := A) Q ((aeval x : (a : K[X]) → A) m : A)
⊢ False

Tactic:
exact hm this
-- Module: Mathlib.RingTheory.Unramified.Finite
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
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)
⊢ 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)

Tactic:
rw [formallyUnramified_iff, KaehlerDifferential,
    Ideal.cotangent_subsingleton_iff, Ideal.isIdempotentElem_iff_of_fg _
      (KaehlerDifferential.ideal_fg R S)]

Premises used: Algebra.formallyUnramified_iff, KaehlerDifferential.ideal_fg, Ideal.isIdempotentElem_iff_of_fg, KaehlerDifferential, Ideal.cotangent_subsingleton_iff
-- Module: Mathlib.RingTheory.Unramified.Finite
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
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:
simp only [KaehlerDifferential.ideal, RingHom.mem_ker, map_sub, map_one,
      sub_eq_zero, @eq_comm S 1]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, KaehlerDifferential.ideal, eq_comm, map_one
-- Module: Mathlib.RingTheory.Unramified.Finite
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
⊢ ∀ (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]