F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
⊢ ¬n = 0 → IsUnit f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
⊢ IsUnit f ∨ n = 0
rw [or_iff_not_imp_right]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
⊢ IsUnit f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
⊢ ¬n = 0 → IsUnit f
rintro hn : n ≠ 0
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
⊢ IsUnit f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
⊢ IsUnit f
have hf2 : derivative (expand F (p ^ n) f) = 0 := by
  rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn.bot_lt,
    MulZeroClass.zero_mul, MulZeroClass.mul_zero]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ∃ r, IsUnit r ∧ ↑C r = ↑(expand F (p ^ n)) f
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
⊢ IsUnit f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
⊢ IsUnit f
rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf
case intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : ↑C r = ↑(expand F (p ^ n)) f
⊢ IsUnit f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ∃ r, IsUnit r ∧ ↑C r = ↑(expand F (p ^ n)) f
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
⊢ IsUnit f
rcases hf with ⟨r, hr, hrf⟩
case intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : f = ↑C r
⊢ IsUnit f
case intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : ↑C r = ↑(expand F (p ^ n)) f
⊢ IsUnit f
rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf
no goals
case intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : f = ↑C r
⊢ IsUnit f
rwa [hrf, isUnit_C]
no goals
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
⊢ ↑derivative (↑(expand F (p ^ n)) f) = 0
rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn.bot_lt,
  MulZeroClass.zero_mul, MulZeroClass.mul_zero]