-- Mathlib/FieldTheory/Finite/Basic.lean
theorem roots_X_pow_card_sub_X : roots (X ^ q - X : K[X]) = Finset.univ.val

Proof state:
case h.e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ derivative (X ^ q - X) = -1

Tactic:
rw [derivative_sub, derivative_X, derivative_X_pow, Nat.cast_card_eq_zero K, C_0,
  zero_mul, zero_sub]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ (X ^ q - X).roots = univ.val

Tactic:
classical
  have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
  have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ := by
    rw [eq_univ_iff_forall]
    intro x
    rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X,
      sub_eq_zero, pow_card]
  rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]
  apply nodup_roots
  rw [separable_def]
  convert isCoprime_one_right.neg_right (R := K[X]) using 1
  rw [derivative_sub, derivative_X, derivative_X_pow, Nat.cast_card_eq_zero K, C_0,
    zero_mul, zero_sub]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots.Nodup

Tactic:
apply nodup_roots

Result:
case hsep
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).Separable

Proof state:
case hsep
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ IsCoprime (X ^ q - X) (derivative (X ^ q - X))

Tactic:
convert isCoprime_one_right.neg_right (R := K[X]) using 1

Result:
case h.e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ derivative (X ^ q - X) = -1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
⊢ (X ^ q - X).roots = univ.val

Tactic:
have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ := by
  rw [eq_univ_iff_forall]
  intro x
  rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X,
    sub_eq_zero, pow_card]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots = univ.val

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
⊢ ∀ (x : K), x ∈ (X ^ q - X).roots.toFinset

Tactic:
intro x

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ x ∈ (X ^ q - X).roots.toFinset

Proof state:
case hsep
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).Separable

Tactic:
rw [separable_def]

Result:
case hsep
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ IsCoprime (X ^ q - X) (derivative (X ^ q - X))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
⊢ (X ^ q - X).roots.toFinset = univ

Tactic:
rw [eq_univ_iff_forall]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
⊢ ∀ (x : K), x ∈ (X ^ q - X).roots.toFinset

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ (X ^ q - X).roots = univ.val

Tactic:
have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
⊢ (X ^ q - X).roots = univ.val

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots = univ.val

Tactic:
rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots.Nodup

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ x ∈ (X ^ q - X).roots.toFinset

Tactic:
rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X,
  sub_eq_zero, pow_card]

Result:
no goals