-- Mathlib/FieldTheory/Separable.lean
theorem isUnit_or_eq_zero_of_separable_expand {f : F[X]} (n : ℕ) (hp : 0 < p)
    (hf : (expand F (p ^ n) f).Separable) : IsUnit f ∨ n = 0

Proof state:
case intro.intro
F : Type u
inst✝ : Field F
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

Tactic:
rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf

Result:
case intro.intro
F : Type u
inst✝ : Field F
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

Proof state:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
⊢ IsUnit f

Tactic:
rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf

Result:
F : Type u
inst✝ : Field F
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

Proof state:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
⊢ derivative ((expand F (p ^ n)) f) = 0

Tactic:
rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
⊢ IsUnit f ∨ n = 0

Tactic:
rw [or_iff_not_imp_right]

Result:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
⊢ ¬n = 0 → IsUnit f

Proof state:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
⊢ IsUnit f

Tactic:
have hf2 : derivative (expand F (p ^ n) f) = 0 := by
  rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]

Result:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
⊢ IsUnit f

Proof state:
case intro.intro
F : Type u
inst✝ : Field F
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

Tactic:
rwa [hrf, isUnit_C]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
⊢ ¬n = 0 → IsUnit f

Tactic:
rintro hn : n ≠ 0

Result:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
⊢ IsUnit f

Proof state:
F : Type u
inst✝ : Field F
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

Tactic:
rcases hf with ⟨r, hr, hrf⟩

Result:
case intro.intro
F : Type u
inst✝ : Field F
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