-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_one_iff_of_monic' (q : ℕ) [ExpChar F q] (hm : f.Monic)
    (hi : Irreducible f) : f.natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F), f = expand F (q ^ n) (X - C y)

Proof state:
case refine_1
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 = (expand F (q ^ n)) (X - C y)

Tactic:
obtain ⟨g, h1, n, rfl⟩ := hi.hasSeparableContraction q

Result:
case refine_1.intro.intro.intro
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) g = (expand F (q ^ n_1)) (X - C y)

Proof state:
case refine_1.intro.intro.intro
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) g = (expand F (q ^ n_1)) (X - C y)

Tactic:
rw [((monic_expand_iff <| expChar_pow_pos F q n).mp hm).eq_X_add_C h2]

Result:
case refine_1.intro.intro.intro
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) (X + C (g.coeff 0)) = (expand F (q ^ n_1)) (X - C y)

Proof state:
case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
x✝ : ∃ n y, f = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : f = (expand F (q ^ n)) (X - C y)
⊢ f.natSepDegree = 1

Tactic:
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ (expand F (q ^ n)) (X + C (g.coeff 0)) = (expand F (q ^ n)) (X - C (-g.coeff 0))

Tactic:
rw [map_neg, sub_neg_eq_add]

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) (X + C (g.coeff 0)) = (expand F (q ^ n_1)) (X - C y)

Tactic:
exact ⟨n, -(g.coeff 0), by rw [map_neg, sub_neg_eq_add]⟩

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
⊢ g.natDegree = 1

Tactic:
rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) g = (expand F (q ^ n_1)) (X - C y)

Tactic:
have h2 : g.natDegree = 1 := by
  rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h

Result:
case refine_1.intro.intro.intro
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) g = (expand F (q ^ n_1)) (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
⊢ f.natSepDegree = 1 ↔ ∃ n y, f = (expand F (q ^ n)) (X - C y)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩

Result:
case refine_1
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 = (expand F (q ^ n)) (X - C y)

case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
x✝ : ∃ n y, f = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : f = (expand F (q ^ n)) (X - C y)
⊢ f.natSepDegree = 1