awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
inst_7 : Field E
inst_8 : Algebra F E
q : ℕ
inst_9 : ExpChar F q
_ : ∀ [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∀ [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
_
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
inst_7 : Field E
inst_8 : Algebra F E
q : ℕ
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
_ : ∀ [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∀ [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
_
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
inst_7 : Field E
inst_8 : Algebra F E
q : ℕ
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
generalize : ∀ (d : ℕ) (hd : finrank F E = d), ∃ (n : ℕ), d = q ^ n
⊢ ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
generalize hd : finrank F E = d

Premises used: Module.finrank
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
pos : ∀ (h : Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤), ∃ (n : ℕ), d = q ^ n
neg : ∀ (h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤), ∃ (n : ℕ), d = q ^ n
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
by_cases h : (⊥ : IntermediateField F E) = ⊤

Premises used: Bot.bot
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
⊢ 1 = d

Tactic:
rw [← finrank_top', ← h, IntermediateField.finrank_bot] at hd

Premises used: IntermediateField.finrank_bot, IntermediateField.finrank_top'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
hd₁ : 1 = d
⊢ Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤

Tactic:
rw [← finrank_top', ← h, IntermediateField.finrank_bot] at hd

Premises used: IntermediateField.finrank_bot, IntermediateField.finrank_top'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : 1 = d
h : Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
⟨0, ((pow_zero q).trans hd).symm⟩

Premises used: pow_zero, Exists.intro, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : 1 = d
h : Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
exact ⟨0, ((pow_zero q).trans hd).symm⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
neg : ∀ (x : E) (hx : x ∉ ⊥), ∃ (n : ℕ), d = q ^ n
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
obtain ⟨x, -, hx⟩ := SetLike.exists_of_lt (lt_of_le_of_ne bot_le h :)

Premises used: SetLike.exists_of_lt, bot_le, lt_of_le_of_ne
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
neg :
  ∀ (m : ℕ) (y : F)
    (e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])),
    ∃ (n : ℕ), d = q ^ n
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
obtain ⟨m, y, e⟩ := IsPurelyInseparable.minpoly_eq_X_pow_sub_C F q x

Premises used: IsPurelyInseparable.minpoly_eq_X_pow_sub_C
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
rw : natDegree (minpoly F x) = q ^ m
rw₁ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])).natDegree = q ^ m
rw₂ : (HPow.hPow (α := F[X]) X (q ^ m)).natDegree = q ^ m
rw₃ rw₄ : q ^ m = q ^ m
⊢ finrank F ↥F⟮x⟯ = q ^ m

Tactic:
rw [adjoin.finrank (Algebra.IsIntegral.isIntegral x), e, natDegree_sub_C, natDegree_X_pow]

Premises used: IntermediateField.adjoin.finrank, Algebra.IsIntegral.isIntegral, Polynomial.natDegree_X_pow, Polynomial.natDegree_sub_C
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
⊢ finrank F ↥F⟮x⟯ = q ^ m

Tactic:
have : finrank F F⟮x⟯ = q ^ m := by
      rw [adjoin.finrank (Algebra.IsIntegral.isIntegral x), e, natDegree_sub_C, natDegree_X_pow]
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
rw : 1 < q ^ m
⊢ finrank (↥F⟮x⟯) E < d

Tactic:
rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]

Premises used: Membership.mem, Subtype, Nat.lt_mul_iff_one_lt_left, Module.finrank_mul_finrank, IntermediateField.adjoin, Singleton.singleton, Module.finrank_pos
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
by_contra! : ∀ (H : q ^ m ≤ 1), False
⊢ 1 < q ^ m

Tactic:
by_contra! H
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
H : q ^ m ≤ 1
⊢ False

Tactic:
hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))

Premises used: le_antisymm, Iff.mp, IntermediateField.finrank_adjoin_simple_eq_one_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
H : q ^ m ≤ 1
refine : 1 ≤ finrank F ↥F⟮x⟯
⊢ False

Tactic:
refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))

Premises used: le_antisymm, Iff.mp, IntermediateField.finrank_adjoin_simple_eq_one_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
H : q ^ m ≤ 1
⊢ 1 ≤ finrank F ↥F⟮x⟯

Tactic:
Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne'

Premises used: Iff.mpr, LT.lt.ne', Nat.one_le_iff_ne_zero, Module.finrank_pos
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
H : q ^ m ≤ 1
⊢ 1 ≤ finrank F ↥F⟮x⟯

Tactic:
exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne'

Premises used: Iff.mpr, LT.lt.ne', Nat.one_le_iff_ne_zero, Module.finrank_pos
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
neg : ∀ (n : ℕ) (hn : finrank (↥F⟮x⟯) E = q ^ n), ∃ (n : ℕ), d = q ^ n
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
obtain ⟨n, hn⟩ := IH _ (by
      rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]
      by_contra! H
      refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))
      exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne') (F⟮x⟯) rfl

Premises used: Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
n : ℕ
hn : finrank (↥F⟮x⟯) E = q ^ n
rw : finrank F E = q ^ (m + n)
rw₁ : finrank F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E = q ^ (m + n)
rw₂ : finrank F ↥F⟮x⟯ * q ^ n = q ^ (m + n)
rw₃ : finrank F ↥F⟮x⟯ * q ^ n = q ^ m * q ^ n
rw₄ rw₅ : q ^ m * q ^ n = q ^ m * q ^ n
⊢ d = q ^ (m + n)

Tactic:
rw [← hd, ← finrank_mul_finrank F F⟮x⟯, hn, pow_add, this]

Premises used: pow_add, Membership.mem, Subtype, Module.finrank_mul_finrank, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
E : Type v
inst_6 : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n
F : Type v
inst_7 : Field F
inst_8 : Algebra F E
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
hd : finrank F E = d
h : ¬Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ m)) ((C : (a : F) → F[X]) y : F[X])
this : finrank F ↥F⟮x⟯ = q ^ m
n : ℕ
hn : finrank (↥F⟮x⟯) E = q ^ n
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
exact ⟨m + n, by rw [← hd, ← finrank_mul_finrank F F⟮x⟯, hn, pow_add, this]⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
inst_7 : Field E
inst_8 : Algebra F E
q : ℕ
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
d : ℕ
hd : finrank F E = d
ind :
  ∀ (d : ℕ)
    (IH :
      ∀ m < d,
        ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
          [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n)
    (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
    [FiniteDimensional F E] (hd : finrank F E = d), ∃ (n : ℕ), d = q ^ n
⊢ ∃ (n : ℕ), d = q ^ n

Tactic:
induction d using Nat.strongRecOn generalizing F with
  | ind d IH =>
    by_cases h : (⊥ : IntermediateField F E) = ⊤
    · rw [← finrank_top', ← h, IntermediateField.finrank_bot] at hd
      exact ⟨0, ((pow_zero q).trans hd).symm⟩
    obtain ⟨x, -, hx⟩ := SetLike.exists_of_lt (lt_of_le_of_ne bot_le h :)
    obtain ⟨m, y, e⟩ := IsPurelyInseparable.minpoly_eq_X_pow_sub_C F q x
    have : finrank F F⟮x⟯ = q ^ m := by
      rw [adjoin.finrank (Algebra.IsIntegral.isIntegral x), e, natDegree_sub_C, natDegree_X_pow]
    obtain ⟨n, hn⟩ := IH _ (by
      rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]
      by_contra! H
      refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))
      exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne') (F⟮x⟯) rfl
    exact ⟨m + n, by rw [← hd, ← finrank_mul_finrank F F⟮x⟯, hn, pow_add, this]⟩

Premises used: Bot.bot, IntermediateField.finrank_bot, IntermediateField.finrank_top'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
pos : ∀ (H : Algebra.IsAlgebraic F E), IsPurelyInseparable F E
neg : ∀ (H : ¬Algebra.IsAlgebraic F E), IsPurelyInseparable F E
⊢ IsPurelyInseparable F E

Tactic:
by_cases H : Algebra.IsAlgebraic F E

Premises used: Algebra.IsAlgebraic
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
pos :
  ∀ (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
⊢ IsPurelyInseparable F E

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 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
⊢ ∀ (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)

Tactic:
fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, fun hsep ↦ ?_⟩

Premises used: Algebra.IsIntegral.isIntegral, And.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
pos :
  ∀ (x : E) (hsep : 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)

Tactic:
refine fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, fun hsep ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
⊢ finSepDegree.{u, v} F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = finSepDegree F E

Tactic:
have := finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E