-- Mathlib/FieldTheory/JacobsonNoether.lean
/-- If `D` is a purely inseparable extension of `k` with characteristic `p`,
  then for every element `a` of `D`, there exists a natural number `n`
  such that `a ^ (p ^ n)` is contained in `k`. -/
lemma exists_pow_mem_center_of_inseparable (p : ℕ) [hchar : ExpChar D p] (a : D)
    (hinsep : ∀ x : D, IsSeparable k x → x ∈ k) : ∃ n, a ^ (p ^ n) ∈ k

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
x : D
hx : IsSeparable (↥k) x
⊢ x ∈ (algebraMap (↥k) D).range

Tactic:
rw [RingHom.mem_range, Subtype.exists]

Result:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
x : D
hx : IsSeparable (↥k) x
⊢ ∃ a, ∃ (b : a ∈ k), (algebraMap (↥k) D) ⟨a, b⟩ = x

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
x : D
hx : IsSeparable (↥k) x
⊢ ∃ a, ∃ (b : a ∈ k), (algebraMap (↥k) D) ⟨a, b⟩ = x

Tactic:
exact ⟨x, ⟨hinsep x hx, rfl⟩⟩

Result:
no goals

Proof state:
case intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this✝ : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
pure : IsPurelyInseparable (↥k) D
n : ℕ
m : ↥k
hm : (algebraMap (↥k) D) m = a ^ p ^ n
this : Set.range ⇑(algebraMap (↥k) D) ⊆ ↑{ toSubsemiring := k.toSubsemiring, algebraMap_mem' := ⋯ }
⊢ ∃ n, a ^ p ^ n ∈ k

Tactic:
exact ⟨n, Set.mem_of_subset_of_mem this <| Set.mem_range.2 ⟨m, hm⟩⟩

Result:
no goals

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
pure : IsPurelyInseparable (↥k) D
⊢ ∃ n, a ^ p ^ n ∈ k

Tactic:
obtain ⟨n, ⟨m, hm⟩⟩ := this pure a

Result:
case intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
pure : IsPurelyInseparable (↥k) D
n : ℕ
m : ↥k
hm : (algebraMap (↥k) D) m = a ^ p ^ n
⊢ ∃ n, a ^ p ^ n ∈ k

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
⊢ ∃ n, a ^ p ^ n ∈ k

Tactic:
have := (@isPurelyInseparable_iff_pow_mem k D _ _ _ _ p (ExpChar.expChar_center_iff.2 hchar)).1

Result:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
⊢ ∃ n, a ^ p ^ n ∈ k

Proof state:
case intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
pure : IsPurelyInseparable (↥k) D
n : ℕ
m : ↥k
hm : (algebraMap (↥k) D) m = a ^ p ^ n
⊢ ∃ n, a ^ p ^ n ∈ k

Tactic:
have := Subalgebra.range_subset (R := k) ⟨(k).toSubsemiring, fun r ↦ r.2⟩

Result:
case intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this✝ : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
pure : IsPurelyInseparable (↥k) D
n : ℕ
m : ↥k
hm : (algebraMap (↥k) D) m = a ^ p ^ n
this : Set.range ⇑(algebraMap (↥k) D) ⊆ ↑{ toSubsemiring := k.toSubsemiring, algebraMap_mem' := ⋯ }
⊢ ∃ n, a ^ p ^ n ∈ k

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
⊢ ∃ n, a ^ p ^ n ∈ k

Tactic:
have pure : IsPurelyInseparable k D := ⟨Algebra.IsAlgebraic.isIntegral, fun x hx ↦ by
  rw [RingHom.mem_range, Subtype.exists]
  exact ⟨x, ⟨hinsep x hx, rfl⟩⟩⟩

Result:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
pure : IsPurelyInseparable (↥k) D
⊢ ∃ n, a ^ p ^ n ∈ k