awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ natDegree (minpoly F α)

Tactic:
natDegree_le_of_dvd key (minpoly.ne_zero hα)

Premises used: Polynomial.natDegree_le_of_dvd, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ natDegree (minpoly F α)

Tactic:
exact natDegree_le_of_dvd key (minpoly.ne_zero hα)

Premises used: Polynomial.natDegree_le_of_dvd, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
h : minpoly F α ∣ p
⊢ natDegree (minpoly F α) = p.natDegree

Tactic:
suffices minpoly F α ∣ p by
    have key := (minpoly.irreducible hα).dvd_symm p_irr this
    apply le_antisymm
    · exact natDegree_le_of_dvd this p_irr.ne_zero
    · exact natDegree_le_of_dvd key (minpoly.ne_zero hα)
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
h : Eq (α := p.SplittingField) ((aeval α : (a : F[X]) → p.SplittingField) p) 0
⊢ minpoly F α ∣ p

Tactic:
apply minpoly.dvd F α

Premises used: minpoly.dvd
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
h : eval α (map (algebraMap F p.SplittingField) p) = 0
h₁ h₂ : Eq.{u_1 + 1} (α := p.SplittingField) 0 0
⊢ Eq (α := p.SplittingField) ((aeval α : (a : F[X]) → p.SplittingField) p) 0

Tactic:
rw [← eval_map_algebraMap, eval_rootOfSplits]

Premises used: Polynomial.eval_map_algebraMap, Polynomial.eval_rootOfSplits
-- Module: Mathlib.FieldTheory.PrimeField
Goal:
⊢ Subsingleton (Subfield ℚ)

Tactic:
subsingleton_of_top_le_bot fun x _ ↦
  have h := Subsingleton.elim ((⊥ : Subfield ℚ).subtype.comp (Rat.castHom _)) (.id _ : ℚ →+* ℚ)
  (congr($h x) : _ = x) ▸ Subtype.prop _

Premises used: Subfield.subtype, subsingleton_of_top_le_bot, Rat, Membership.mem, Subtype, Bot.bot, RingHom.comp, Rat.castHom, Subsingleton.elim, RingHom.id
-- Module: Mathlib.FieldTheory.PrimeField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Subsingleton (Subfield (ZMod p))

Tactic:
subsingleton_of_top_le_bot fun x _ ↦
    have h := Subsingleton.elim ((⊥ : Subfield (ZMod p)).subtype.comp
      (ZMod.castHom dvd_rfl _)) (.id _ : ZMod p →+* ZMod p)
    (congr($h x) : _ = x) ▸ Subtype.prop _

Premises used: Subfield.subtype, subsingleton_of_top_le_bot, Membership.mem, Subtype, Bot.bot, ZMod, RingHom.comp, dvd_rfl, Subsingleton.elim, RingHom.id, ZMod.castHom
-- Module: Mathlib.FieldTheory.PrimeField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
rw : Eq (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
rw₁ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
rw₂ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (map (algebraMap ℚ K) ⊥)
rw₃ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (map (algebraMap ℚ K) ⊤)
rw₄ rw₅ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (RingHom.fieldRange (algebraMap ℚ K))
⊢ Eq (α := Subfield K) ⊥ (RingHom.fieldRange (algebraMap ℚ K))

Tactic:
rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]

Premises used: Iff.mpr, Algebra.algebraMap, Rat, inferInstance, Subfield.map_bot, eq_comm, RingHom.fieldRange_eq_map, subsingleton_iff_bot_eq_top, eq_bot_iff
-- Module: Mathlib.FieldTheory.PrimeField
Goal:
K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst : Field K
inst_1 : Algebra (ZMod p) K
rw : Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
rw₁ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
rw₂ :
  LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
    (map (K := ZMod p) (algebraMap (ZMod p) K) ⊥)
rw₃ :
  LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
    (map (K := ZMod p) (algebraMap (ZMod p) K) ⊤)
rw₄ rw₅ :
  LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
    (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
⊢ Eq.{u_1 + 1} (α := Subfield K) ⊥ (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))

Tactic:
rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap (ZMod p) K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]

Premises used: Iff.mpr, Algebra.algebraMap, inferInstance, Subfield.map_bot, eq_comm, ZMod, RingHom.fieldRange_eq_map, subsingleton_iff_bot_eq_top, eq_bot_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
x : E
⊢ IsIntegral F x

Tactic:
Algebra.IsIntegral.isIntegral _

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
inst_3 : Nontrivial F
inst_4 : IsPurelyInseparable F E
⊢ Algebra.IsAlgebraic F E

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
⊢ ∀ (x : E), IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F E)) x

Tactic:
IsPurelyInseparable.inseparable'

Premises used: IsPurelyInseparable.inseparable'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
⊢ IsPurelyInseparable F E ↔
    ∀ (x : E),
      IsIntegral F x ∧
        (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F E)) x)

Tactic:
⟨fun h x ↦ ⟨h.isIntegral' _ x, h.inseparable' x⟩, fun h ↦ ⟨⟨fun x ↦ (h x).1⟩, fun x ↦ (h x).2⟩⟩

Premises used: IsPurelyInseparable.inseparable', IsPurelyInseparable.isIntegral', IsPurelyInseparable.mk, And.right, And.left, And.intro, Iff.intro, Algebra.IsIntegral.mk
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
x : E
rw : IsIntegral.{u_1, u_3} F (A := K) ((e.symm : (a : E) → K) x : K)
⊢ IsIntegral F x

Tactic:
rw [← isIntegral_algEquiv e.symm]

Premises used: AlgEquiv.symm, isIntegral_algEquiv
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
x : E
⊢ IsIntegral.{u_1, u_3} F (A := K) ((e.symm : (a : E) → K) x : K)

Tactic:
IsPurelyInseparable.isIntegral' F _

Premises used: IsPurelyInseparable.isIntegral'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
x : E
⊢ IsIntegral.{u_1, u_3} F (A := K) ((e.symm : (a : E) → K) x : K)

Tactic:
exact IsPurelyInseparable.isIntegral' F _

Premises used: IsPurelyInseparable.isIntegral'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
refine :
  ∀ (x : E) (h : IsSeparable F x),
    Membership.mem (γ := Subring E) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F E)) x
⊢ IsPurelyInseparable F E

Tactic:
refine ⟨⟨fun _ ↦ by rw [← isIntegral_algEquiv e.symm]; exact IsPurelyInseparable.isIntegral' F _⟩,
    fun x h ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ Separable (minpoly.{u_1, u_3} F (B := K) ((e.symm : (a : E) → K) x : K))

Tactic:
rw [IsSeparable, ← minpoly.algEquiv_eq e.symm] at h

Premises used: AlgEquiv.symm, minpoly.algEquiv_eq, IsSeparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
x : E
h : Separable (minpoly.{u_1, u_3} F (B := K) ((e.symm : (a : E) → K) x : K))
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F E)) x

Tactic:
simpa only [RingHom.mem_range, algebraMap_eq_apply] using IsPurelyInseparable.inseparable F _ h

Premises used: RingHom.mem_range, AlgEquiv.algebraMap_eq_apply, IsPurelyInseparable.inseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
⊢ IsPurelyInseparable F K ↔ IsPurelyInseparable F E

Tactic:
⟨fun _ ↦ e.isPurelyInseparable, fun _ ↦ e.symm.isPurelyInseparable⟩

Premises used: AlgEquiv.symm, AlgEquiv.isPurelyInseparable, Iff.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : CommRing F_1
inst_1 : Ring E_1
inst_2 : Algebra F_1 E_1
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F_1 K
F : Type u
E : Type v
inst_5 : Field F
inst_6 : Ring E
inst_7 : IsDomain E
inst_8 : Algebra F E
inst_9 : Algebra.IsAlgebraic F E
inst_10 : IsSepClosed F
⊢ IsPurelyInseparable F E

Tactic:
⟨inferInstance, fun x h ↦ minpoly.mem_range_of_degree_eq_one F x <|
    IsSepClosed.degree_eq_one_of_irreducible F (minpoly.irreducible
      (Algebra.IsIntegral.isIntegral _)) h⟩

Premises used: Algebra.IsIntegral.isIntegral, inferInstance, IsPurelyInseparable.mk, minpoly.mem_range_of_degree_eq_one, IsSepClosed.degree_eq_one_of_irreducible, minpoly.irreducible
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
inst_4 : Algebra.IsSeparable F E
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
fun x ↦ IsPurelyInseparable.inseparable F x (Algebra.IsSeparable.isSeparable F x)

Premises used: Algebra.IsSeparable.isSeparable, Set.Mem, setOf, Set.range, Function.Surjective, IsPurelyInseparable.inseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
inst_3 : Nontrivial E
inst_4 : IsDomain F
inst_5 : IsTorsionFree F E
inst_6 : IsPurelyInseparable F E
inst_7 : Algebra.IsSeparable F E
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
⟨FaithfulSMul.algebraMap_injective F E, surjective_algebraMap_of_isSeparable F E⟩

Premises used: IsPurelyInseparable.surjective_algebraMap_of_isSeparable, FaithfulSMul.algebraMap_injective, And.intro, Function.Bijective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
L : Subalgebra F E
inst_3 : IsPurelyInseparable.{u_1, u_2} F ↥L
inst_4 : Algebra.IsSeparable.{u_1, u_2} F ↥L
x : E
hx : x ∈ L
obtain :
  ∀ (y : F) (hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx),
    Membership.mem (γ := Subalgebra F E) ⊥ x
⊢ Membership.mem (γ := Subalgebra F E) ⊥ x

Tactic:
obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩

Premises used: Membership.mem, IsPurelyInseparable.surjective_algebraMap_of_isSeparable, Subtype, Subtype.mk
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
L : Subalgebra F E
inst_3 : IsPurelyInseparable.{u_1, u_2} F ↥L
inst_4 : Algebra.IsSeparable.{u_1, u_2} F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx
⊢ Membership.mem (γ := Subalgebra F E) ⊥ x

Tactic:
⟨y, congr_arg (Subalgebra.val _) hy⟩

Premises used: Set.Mem, Subalgebra.val, setOf, congr_arg, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
L : Subalgebra F E
inst_3 : IsPurelyInseparable.{u_1, u_2} F ↥L
inst_4 : Algebra.IsSeparable.{u_1, u_2} F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx
⊢ Membership.mem (γ := Subalgebra F E) ⊥ x

Tactic:
exact ⟨y, congr_arg (Subalgebra.val _) hy⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : IsPurelyInseparable.{u, v} F ↥L
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
x : E
hx : x ∈ L
obtain :
  ∀ (y : F) (hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx),
    Membership.mem (γ := IntermediateField F E) ⊥ x
⊢ Membership.mem (γ := IntermediateField F E) ⊥ x

Tactic:
obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩

Premises used: Membership.mem, IsPurelyInseparable.surjective_algebraMap_of_isSeparable, Subtype, Subtype.mk
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : IsPurelyInseparable.{u, v} F ↥L
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx
⊢ Membership.mem (γ := IntermediateField F E) ⊥ x

Tactic:
⟨y, congr_arg (algebraMap L E) hy⟩

Premises used: Algebra.algebraMap, Set.Mem, setOf, Membership.mem, Subtype, congr_arg, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : IsPurelyInseparable.{u, v} F ↥L
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx
⊢ Membership.mem (γ := IntermediateField F E) ⊥ x

Tactic:
exact ⟨y, congr_arg (algebraMap L E) hy⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
⊢ Eq (α := IntermediateField F E) (separableClosure F E) ⊥

Tactic:
bot_unique fun x h ↦ IsPurelyInseparable.inseparable F x (mem_separableClosure_iff.1 h)

Premises used: Iff.mp, bot_unique, mem_separableClosure_iff, IsPurelyInseparable.inseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥
x : E
hs : IsSeparable F x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
simpa only [h] using mem_separableClosure_iff.2 hs

Premises used: Iff.mpr, mem_separableClosure_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
⊢ IsPurelyInseparable F F

Tactic:
⟨inferInstance, fun x _ ↦ ⟨x, rfl⟩⟩

Premises used: inferInstance, IsPurelyInseparable.mk, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
rw :
  (∀ (x : E),
      IsIntegral F x ∧
        (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)) ↔
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
⊢ IsPurelyInseparable F E ↔
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
rw [isPurelyInseparable_iff]

Premises used: isPurelyInseparable_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
⊢ (∀ (x : E),
      IsIntegral F x ∧
        (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)) ↔
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
⟨fun h x ↦ ?_, fun h x ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
refine_1 :
  ∀
    (h :
      ∀ (x : E),
        IsIntegral F x ∧
          (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x))
    (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
refine_2 :
  ∀
    (h :
      ∀ (x : E),
        ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n))
    (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
⊢ (∀ (x : E),
      IsIntegral F x ∧
        (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)) ↔
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h :
  ∀ (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
x : E
refine_1 :
  ∀ (g : F[X]) (h1 : g.Separable) (n : ℕ)
    (h2 : Eq (α := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X]) (minpoly F x : F[X])),
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
obtain ⟨g, h1, n, h2⟩ := (minpoly.irreducible (h x).1).hasSeparableContraction q

Premises used: Irreducible.hasSeparableContraction, And.left, minpoly.irreducible
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h :
  ∀ (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
x : E
g : F[X]
h1 : g.Separable
n : ℕ
h2 : Eq (α := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X]) (minpoly F x : F[X])
⊢ Eq.{v + 1} (α := E) ((aeval (x ^ q ^ n) : (a : F[X]) → E) g : E) (0 : E)

Tactic:
simpa only [expand_aeval, minpoly.aeval] using congr_arg (aeval x) h2

Premises used: minpoly.aeval, congr_arg, Polynomial.aeval, Polynomial.expand_aeval, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h :
  ∀ (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
x : E
g : F[X]
h1 : g.Separable
n : ℕ
h2 : Eq (α := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X]) (minpoly F x : F[X])
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
exact ⟨n, (h _).2 <| h1.of_dvd <| minpoly.dvd F _ <| by
      simpa only [expand_aeval, minpoly.aeval] using congr_arg (aeval x) h2⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
⊢ natSepDegree (minpoly F x) = 1

Tactic:
have hdeg := (minpoly.natSepDegree_eq_one_iff_pow_mem q).2 (h x)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
h' : ¬IsIntegral F x
⊢ False

Tactic:
simp only [minpoly.eq_zero h', natSepDegree_zero, zero_ne_one] at hdeg

Premises used: Polynomial.natSepDegree_zero, zero_ne_one, minpoly.eq_zero
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
⊢ IsIntegral F x

Tactic:
have halg : IsIntegral F x := by_contra fun h' ↦ by
    simp only [minpoly.eq_zero h', natSepDegree_zero, zero_ne_one] at hdeg
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
halg : IsIntegral F x
⊢ IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)

Tactic:
⟨halg, fun hsep ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
halg : IsIntegral F x
refine_2 :
  ∀ (hsep : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
⊢ IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)

Tactic:
refine ⟨halg, fun hsep ↦ ?_⟩