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'

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'
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'
wlog hm : m ≤ m'
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'
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'
obtain ⟨s, rfl⟩ := exists_add_of_le hm
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'
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'
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand
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'
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'
subst h_expand
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'

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'
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'
rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)
no goals
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'
exact (this q hf g' g m' m h_expand.symm hg' hg (le_of_not_le hm)).symm
no goals
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'
rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, MulZeroClass.zero_mul]
no goals
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'
rw [natDegree_expand, pow_zero, mul_one]