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

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
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
cases hF
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
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
rcases hg with ⟨_, m, hm⟩
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
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
rw [one_pow, expand_one] at hm
no goals
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
rw [hf.eq_degree, hm]
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
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
rcases hg with ⟨hg, m, hm⟩
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
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
let g' := Classical.choose hf
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
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
cases' (Classical.choose_spec hf).2 with m' hm'
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
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
haveI : Fact q.Prime := ⟨by assumption⟩
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'
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
apply contraction_degree_eq_or_insep q g g' m m'
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'
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'
rw [hm, hm']
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

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'
exact hg
no goals
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'
exact (Classical.choose_spec hf).1
no goals
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
assumption