-- Mathlib/FieldTheory/JacobsonNoether.lean
theorem exists_separable_and_not_isCentral (H : k ≠ (⊤ : Subring D)) :
    ∃ x : D, x ∉ k ∧ IsSeparable k x

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc : c⁻¹ * a = a * c⁻¹
⊢ c⁻¹ * a = a * c⁻¹

Tactic:
exact hc

Result:
no goals

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
⊢ ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n] b ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0

Tactic:
obtain ⟨m, -, hm2⟩ := exist_pow_eq_zero_of_le p ha insep

Result:
case intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
⊢ ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n] b ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : ¬0 < t
h_find : Nat.find h_exist = 1
⊢ (⇑((ad (↥k) D) a))^[Nat.find h_exist] b ≠ 0

Tactic:
rwa [h_find]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ False

Tactic:
have hc : a * c = c * a := by
  apply eq_of_sub_eq_zero
  rw [← mulLeft_apply (R := k), ← mulRight_apply (R := k)]
  suffices ad k D a c = 0 from by
    rw [← this]; rfl
  rw [← Function.iterate_succ_apply' (ad k D a) n b, hb.2]

Result:
case intro.intro.intro.intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
⊢ False

Proof state:
case h
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ ((ad (↥k) D) a) c = 0

Tactic:
rw [← Function.iterate_succ_apply' (ad k D a) n b, hb.2]

Result:
no goals

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ a * c = c * a

Tactic:
apply eq_of_sub_eq_zero

Result:
case h
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ a * c - c * a = 0

Proof state:
case h.e'_2.h.e'_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : 0 < t
⊢ Nat.find h_exist = t + 1

Tactic:
omega

Result:
no goals

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * d - d * a = a

Tactic:
nth_rw 3 [← mul_one a]

Result:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * d - d * a = a * 1

Proof state:
case neg
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : ¬0 < t
⊢ (⇑((ad (↥k) D) a))^[Nat.find h_exist] b ≠ 0

Tactic:
suffices h_find: Nat.find h_exist = 1 by
  rwa [h_find]

Result:
case neg
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : ¬0 < t
⊢ Nat.find h_exist = 1