[GOAL]
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f : F[X]
hf✝ : HasSeparableContraction q f
g : F[X]
hf : IsSeparableContraction q f g
⊢ ∃ m, natDegree g * q ^ m = natDegree f
[PROOFSTEP]
obtain ⟨m, rfl⟩ := hf.2
[GOAL]
case intro
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf✝ : HasSeparableContraction q (↑(expand F (q ^ m)) g)
hf : IsSeparableContraction q (↑(expand F (q ^ m)) g) g
⊢ ∃ m_1, natDegree g * q ^ m_1 = natDegree (↑(expand F (q ^ m)) g)
[PROOFSTEP]
use m
[GOAL]
case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf✝ : HasSeparableContraction q (↑(expand F (q ^ m)) g)
hf : IsSeparableContraction q (↑(expand F (q ^ m)) g) g
⊢ natDegree g * q ^ m = natDegree (↑(expand F (q ^ m)) g)
[PROOFSTEP]
rw [natDegree_expand]
[GOAL]
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f✝ : F[X]
hf✝ : HasSeparableContraction q f✝
f : F[X]
hf : HasSeparableContraction 1 f
⊢ degree hf = natDegree f
[PROOFSTEP]
let ⟨a, ha⟩ := hf.dvd_degree'
[GOAL]
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f✝ : F[X]
hf✝ : HasSeparableContraction q f✝
f : F[X]
hf : HasSeparableContraction 1 f
a : ℕ
ha : degree hf * 1 ^ a = natDegree f
⊢ degree hf = natDegree f
[PROOFSTEP]
rw [← ha, one_pow a, mul_one]
[GOAL]
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
⊢ HasSeparableContraction q f
[PROOFSTEP]
cases hF
[GOAL]
case zero
F : Type u_1
inst✝¹ : Field F
q : ℕ
f✝ : F[X]
hf : HasSeparableContraction q f✝
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f
[PROOFSTEP]
exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
q : ℕ
f✝ : F[X]
hf : HasSeparableContraction q f✝
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ ↑(expand F (1 ^ 0)) f = f
[PROOFSTEP]
rw [pow_zero, expand_one]
[GOAL]
case prime
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f
[PROOFSTEP]
rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩
[GOAL]
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : Separable g
hge : ↑(expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f
[PROOFSTEP]
exact ⟨g, hgs, n, hge⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
hg : Separable g
hg' : Separable g'
⊢ natDegree g = natDegree g'
[PROOFSTEP]
wlog hm : m ≤ m'
[GOAL]
case inr
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
hg : Separable g
hg' : Separable g'
this :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) {f : F[X]},
    HasSeparableContraction q f →
      ∀ [hq : NeZero q] [inst_1 : CharP F q] (g g' : F[X]) (m m' : ℕ),
        ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g' →
          Separable g → Separable g' → m ≤ m' → natDegree g = natDegree g'
hm : ¬m ≤ m'
⊢ natDegree g = natDegree g'
[PROOFSTEP]
exact (this q hf g' g m' m h_expand.symm hg' hg (le_of_not_le hm)).symm
[GOAL]
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
hg : Separable g
hg' : Separable g'
hm : m ≤ m'
⊢ natDegree g = natDegree g'
[PROOFSTEP]
obtain ⟨s, rfl⟩ := exists_add_of_le hm
[GOAL]
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : Separable g
hg' : Separable g'
s : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ (m + s))) g'
hm : m ≤ m + s
⊢ natDegree g = natDegree g'
[PROOFSTEP]
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand 
[GOAL]
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : Separable g
hg' : Separable g'
s : ℕ
h_expand : g = ↑(expand F (q ^ s)) g'
hm : m ≤ m + s
⊢ natDegree g = natDegree g'
[PROOFSTEP]
subst h_expand
[GOAL]
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : Separable g'
s : ℕ
hm : m ≤ m + s
hg : Separable (↑(expand F (q ^ s)) g')
⊢ natDegree (↑(expand F (q ^ s)) g') = natDegree g'
[PROOFSTEP]
rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)
[GOAL]
case intro.inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : Separable g'
s : ℕ
hm : m ≤ m + s
hg : Separable (↑(expand F (q ^ s)) g')
h : IsUnit g'
⊢ natDegree (↑(expand F (q ^ s)) g') = natDegree g'
[PROOFSTEP]
rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]
[GOAL]
case intro.inr
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : Separable g'
hm : m ≤ m + 0
hg : Separable (↑(expand F (q ^ 0)) g')
⊢ natDegree (↑(expand F (q ^ 0)) g') = natDegree g'
[PROOFSTEP]
rw [natDegree_expand, pow_zero, mul_one]
[GOAL]
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hF : ExpChar F q
g : F[X]
hg : IsSeparableContraction q f g
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
cases hF
[GOAL]
case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
hg : IsSeparableContraction 1 f g
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rcases hg with ⟨_, m, hm⟩
[GOAL]
case zero.intro.intro
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : Separable g
m : ℕ
hm : ↑(expand F (1 ^ m)) g = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rw [one_pow, expand_one] at hm 
[GOAL]
case zero.intro.intro
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : Separable g
m : ℕ
hm : g = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rw [hf.eq_degree, hm]
[GOAL]
case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hg : IsSeparableContraction q f g
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rcases hg with ⟨hg, m, hm⟩
[GOAL]
case prime.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
let g' := Classical.choose hf
[GOAL]
case prime.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
cases' (Classical.choose_spec hf).2 with m' hm'
[GOAL]
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
haveI : Fact q.Prime := ⟨by assumption⟩
[GOAL]
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
⊢ Nat.Prime q
[PROOFSTEP]
assumption
[GOAL]
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
apply contraction_degree_eq_or_insep q g g' m m'
[GOAL]
case prime.intro.intro.intro.h_expand
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
case prime.intro.intro.intro.hg
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g
case prime.intro.intro.intro.hg'
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g'
[PROOFSTEP]
rw [hm, hm']
[GOAL]
case prime.intro.intro.intro.hg
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g
case prime.intro.intro.intro.hg'
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g'
[PROOFSTEP]
exact hg
[GOAL]
case prime.intro.intro.intro.hg'
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g'
[PROOFSTEP]
exact (Classical.choose_spec hf).1
