-- Mathlib/FieldTheory/SeparableDegree.lean
theorem eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one (q : ℕ) [ExpChar F q] (hm : f.Monic)
    (h : f.natSepDegree = 1) : ∃ (m n : ℕ) (y : F),
      m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : c.natDegree = 0
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Tactic:
simpa only [eq_one_of_monic_natDegree_zero ((hM.pow _).of_mul_monic_left (hf ▸ hm)) h,
  mul_one, ← hp] using hf

Result:
no goals

Proof state:
case intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
obtain ⟨n, y, H, hp⟩ := hM.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible q hI hD

Result:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
refine ⟨_, n, y, hne, H, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Tactic:
obtain ⟨c, hf, H⟩ := hF.exists_eq_pow_mul_and_not_dvd

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
have hF := finiteMultiplicity_of_degree_pos_of_monic (degree_pos_of_irreducible hI) hM hm.ne_zero

Result:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
obtain ⟨p, hM, hI, hf⟩ := exists_monic_irreducible_factor _ <| not_isUnit_of_natDegree_pos _
  <| Nat.pos_of_ne_zero <| (natSepDegree_ne_zero_iff _).1 (h.symm ▸ Nat.one_ne_zero)

Result:
case intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
classical
have hne := (multiplicity_pos_of_dvd hf).ne'
refine ⟨_, n, y, hne, H, ?_⟩
obtain ⟨c, hf, H⟩ := hF.exists_eq_pow_mul_and_not_dvd
rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
  (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
  add_right_eq_self, natSepDegree_eq_zero_iff] at h
simpa only [eq_one_of_monic_natDegree_zero ((hM.pow _).of_mul_monic_left (hf ▸ hm)) h,
  mul_one, ← hp] using hf

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
have hne := (multiplicity_pos_of_dvd hf).ne'

Result:
case intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
case intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
have hD := (h ▸ natSepDegree_le_of_dvd p f hf hm.ne_zero).antisymm <|
  Nat.pos_of_ne_zero <| (natSepDegree_ne_zero_iff _).2 hI.natDegree_pos.ne'

Result:
case intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m