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

Proof state:
case intro.intro.prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y

Tactic:
refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩

Result:
case intro.intro.prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
⊢ False

Proof state:
case intro.intro.prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hi : Irreducible ((X ^ q ^ n.pred - C z) ^ q)
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False

Tactic:
exact not_irreducible_pow hq.ne_one hi

Result:
no goals

Proof state:
case intro.intro.zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X - C y

Tactic:
exact ⟨0, y, .inl rfl, hf⟩

Result:
no goals

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

Tactic:
cases id ‹ExpChar F q› with
| zero =>
  simp_rw [one_pow, pow_one] at hf ⊢
  exact ⟨0, y, .inl rfl, hf⟩
| prime hq =>
  refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩
  haveI := expChar_of_injective_ringHom (R := F) C_injective q
  rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow,
    ← sub_pow_expChar] at hi
  exact not_irreducible_pow hq.ne_one hi

Result:
no goals

Proof state:
case intro.intro.prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
⊢ False

Tactic:
haveI := expChar_of_injective_ringHom (R := F) C_injective q

Result:
case intro.intro.prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False

Proof state:
case intro.intro.prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False

Tactic:
rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow,
  ← sub_pow_expChar] at hi

Result:
case intro.intro.prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hi : Irreducible ((X ^ q ^ n.pred - C z) ^ q)
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False

Proof state:
case intro.intro.zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X ^ 1 ^ n - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X ^ 1 ^ n - C y

Tactic:
simp_rw [one_pow, pow_one] at hf ⊢

Result:
case intro.intro.zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X - C y

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

Tactic:
obtain ⟨n, y, hf⟩ := (hm.natSepDegree_eq_one_iff_of_irreducible q hi).1 h

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