no goals
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
⊢ roots (X ^ q - X) = univ.val
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, CharP.cast_card_eq_zero K, C_0,
    MulZeroClass.zero_mul, zero_sub]
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ roots (X ^ q - X) = univ.val
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
⊢ roots (X ^ q - X) = univ.val
have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ roots (X ^ q - X) = univ.val
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ roots (X ^ q - X) = univ.val
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]
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ Multiset.Nodup (roots (X ^ q - X))
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ roots (X ^ q - X) = univ.val
rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]
case hsep
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ Separable (X ^ q - X)
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ Multiset.Nodup (roots (X ^ q - X))
apply nodup_roots
case hsep
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ IsCoprime (X ^ q - X) (↑derivative (X ^ q - X))
case hsep
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ Separable (X ^ q - X)
rw [separable_def]
case h.e'_4
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ ↑derivative (X ^ q - X) = -1
case hsep
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ IsCoprime (X ^ q - X) (↑derivative (X ^ q - X))
convert isCoprime_one_right.neg_right (R := K[X]) using 1
no goals
case h.e'_4
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ ↑derivative (X ^ q - X) = -1
rw [derivative_sub, derivative_X, derivative_X_pow, CharP.cast_card_eq_zero K, C_0,
  MulZeroClass.zero_mul, zero_sub]
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ ∀ (x : K), x ∈ Multiset.toFinset (roots (X ^ q - X))
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ Multiset.toFinset (roots (X ^ q - X)) = univ
rw [eq_univ_iff_forall]
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
x : K
⊢ x ∈ Multiset.toFinset (roots (X ^ q - X))
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ ∀ (x : K), x ∈ Multiset.toFinset (roots (X ^ q - X))
intro x
no goals
K : Type u_1
R : Type ?u.732401
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
x : K
⊢ x ∈ Multiset.toFinset (roots (X ^ q - X))
rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X,
  sub_eq_zero, pow_card]