-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem isPurelyInseparable_iff_pow_mem :
    IsPurelyInseparable F E ↔ ∀ x : E, ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range

Proof state:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Tactic:
have hdeg := (minpoly.natSepDegree_eq_one_iff_pow_mem q).2 (h x)

Result:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Proof state:
case refine_1.intro.intro.intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
g : F[X]
h1 : g.Separable
n : ℕ
h2 : (expand F (q ^ n)) g = minpoly F x
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
exact ⟨n, (h _).2 <| h1.of_dvd <| minpoly.dvd F _ <| by
  simpa only [expand_aeval, minpoly.aeval] using congr_arg (aeval x) h2⟩

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
g : F[X]
h1 : g.Separable
n : ℕ
h2 : (expand F (q ^ n)) g = minpoly F x
⊢ (aeval (x ^ q ^ n)) g = 0

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

Result:
no goals

Proof state:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
hsep : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
rwa [hsep.natSepDegree_eq_natDegree, minpoly.natDegree_eq_one_iff] at hdeg

Result:
no goals

Proof state:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Tactic:
have halg : IsIntegral F x := by_contra fun h' ↦ by
  simp only [minpoly.eq_zero h', natSepDegree_zero, zero_ne_one] at hdeg

Result:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
rw [isPurelyInseparable_iff]

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ (∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)) ↔
    ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
h' : ¬IsIntegral F x
⊢ False

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

Result:
no goals

Proof state:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

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

Result:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
hsep : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ (∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)) ↔
    ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

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

Result:
case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Proof state:
case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

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

Result:
case refine_1.intro.intro.intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
g : F[X]
h1 : g.Separable
n : ℕ
h2 : (expand F (q ^ n)) g = minpoly F x
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range