F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : Nat.Prime p
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : p ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : Nat.Prime p
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
induction' hn : f.natDegree using Nat.strong_induction_on with N ih generalizing f
case h.inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h : Separable f
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f

case h.inr.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
case h.inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h : Separable f
⊢ ↑(expand F (p ^ 0)) f = f
case h.inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h : Separable f
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
refine' ⟨0, f, h, _⟩
no goals
case h.inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h : Separable f
⊢ ↑(expand F (p ^ 0)) f = f
rw [pow_zero, expand_one]
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.zero
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f

case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
cases' N with N
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
have hg2 : g.natDegree ≠ 0 := by
  intro this
  rw [this, MulZeroClass.zero_mul] at hg1
  cases hg1
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
hg3 : natDegree g < Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
have hg3 : g.natDegree < N.succ := by
  rw [← mul_one g.natDegree, ← hg1]
  exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
case h.inr.intro.intro.intro.succ.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
n : ℕ
g : F[X]
hg4 : Separable g
hg : Irreducible (↑(expand F (p ^ n)) g)
hgf : ↑(expand F p) (↑(expand F (p ^ n)) g) = f
hg1 : natDegree (↑(expand F (p ^ n)) g) * p = Nat.succ N
hg2 : natDegree (↑(expand F (p ^ n)) g) ≠ 0
hg3 : natDegree (↑(expand F (p ^ n)) g) < Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
hg3 : natDegree g < Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
case h.inr.intro.intro.intro.succ.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
n : ℕ
g : F[X]
hg4 : Separable g
hg : Irreducible (↑(expand F (p ^ n)) g)
hgf : ↑(expand F p) (↑(expand F (p ^ n)) g) = f
hg1 : natDegree (↑(expand F (p ^ n)) g) * p = Nat.succ N
hg2 : natDegree (↑(expand F (p ^ n)) g) ≠ 0
hg3 : natDegree (↑(expand F (p ^ n)) g) < Nat.succ N
⊢ ↑(expand F (p ^ (n + 1))) g = f
case h.inr.intro.intro.intro.succ.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
n : ℕ
g : F[X]
hg4 : Separable g
hg : Irreducible (↑(expand F (p ^ n)) g)
hgf : ↑(expand F p) (↑(expand F (p ^ n)) g) = f
hg1 : natDegree (↑(expand F (p ^ n)) g) * p = Nat.succ N
hg2 : natDegree (↑(expand F (p ^ n)) g) ≠ 0
hg3 : natDegree (↑(expand F (p ^ n)) g) < Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
refine' ⟨n + 1, g, hg4, _⟩
no goals
case h.inr.intro.intro.intro.succ.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
n : ℕ
g : F[X]
hg4 : Separable g
hg : Irreducible (↑(expand F (p ^ n)) g)
hgf : ↑(expand F p) (↑(expand F (p ^ n)) g) = f
hg1 : natDegree (↑(expand F (p ^ n)) g) * p = Nat.succ N
hg2 : natDegree (↑(expand F (p ^ n)) g) ≠ 0
hg3 : natDegree (↑(expand F (p ^ n)) g) < Nat.succ N
⊢ ↑(expand F (p ^ (n + 1))) g = f
rw [← hgf, expand_expand, pow_succ]
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.zero
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
hf0 : f ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
have hf0 : f ≠ 0 := hf.ne_zero
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = 0
hf0 : f ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
hf0 : f ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
rw [h1, C_0] at hn
no goals
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = 0
hf0 : f ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
exact absurd hn hf0
no goals
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
⊢ natDegree g * p = Nat.succ N
rwa [← natDegree_expand, hgf]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
this : natDegree g = 0
⊢ False
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
⊢ natDegree g ≠ 0
intro this
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : 0 = Nat.succ N
this : natDegree g = 0
⊢ False
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
this : natDegree g = 0
⊢ False
rw [this, MulZeroClass.zero_mul] at hg1
no goals
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : 0 = Nat.succ N
this : natDegree g = 0
⊢ False
cases hg1
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ natDegree g * 1 < natDegree g * p
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ natDegree g < Nat.succ N
rw [← mul_one g.natDegree, ← hg1]
no goals
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ natDegree g * 1 < natDegree g * p
exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt