-- Mathlib/RingTheory/Polynomial/SeparableDegree.lean
theorem contraction_degree_eq_or_insep [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
    (h_expand : expand F (q ^ m) g = expand F (q ^ m') g') (hg : g.Separable) (hg' : g'.Separable) :
    g.natDegree = g'.natDegree

Proof state:
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
⊢ ((expand F (q ^ s)) g').natDegree = g'.natDegree

Tactic:
rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)

Result:
case intro.inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
h : IsUnit g'
⊢ ((expand F (q ^ s)) g').natDegree = g'.natDegree

case intro.inr
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : ((expand F (q ^ 0)) g').Separable
⊢ ((expand F (q ^ 0)) g').natDegree = g'.natDegree

Proof state:
case intro.inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
h : IsUnit g'
⊢ ((expand F (q ^ s)) g').natDegree = g'.natDegree

Tactic:
rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]

Result:
no goals

Proof state:
case inr
F : Type u_1
inst✝¹ : Field F
q : ℕ
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 : g.Separable
hg' : g'.Separable
this :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [inst_1 : CharP F q] (g g' : F[X]) (m m' : ℕ),
    (expand F (q ^ m)) g = (expand F (q ^ m')) g' → g.Separable → g'.Separable → m ≤ m' → g.natDegree = g'.natDegree
hm : ¬m ≤ m'
⊢ g.natDegree = g'.natDegree

Tactic:
exact (this q g' g m' m h_expand.symm hg' hg (le_of_not_le hm)).symm

Result:
no goals

Proof state:
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : g = (expand F (q ^ s)) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree

Tactic:
subst h_expand

Result:
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
⊢ ((expand F (q ^ s)) g').natDegree = g'.natDegree

Proof state:
F : Type u_1
inst✝¹ : Field F
q : ℕ
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 : g.Separable
hg' : g'.Separable
⊢ g.natDegree = g'.natDegree

Tactic:
wlog hm : m ≤ m'

Result:
case inr
F : Type u_1
inst✝¹ : Field F
q : ℕ
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 : g.Separable
hg' : g'.Separable
this :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [inst_1 : CharP F q] (g g' : F[X]) (m m' : ℕ),
    (expand F (q ^ m)) g = (expand F (q ^ m')) g' → g.Separable → g'.Separable → m ≤ m' → g.natDegree = g'.natDegree
hm : ¬m ≤ m'
⊢ g.natDegree = g'.natDegree

F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
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 : g.Separable
hg' : g'.Separable
hm : m ≤ m'
⊢ g.natDegree = g'.natDegree

Proof state:
case intro.inr
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : ((expand F (q ^ 0)) g').Separable
⊢ ((expand F (q ^ 0)) g').natDegree = g'.natDegree

Tactic:
rw [natDegree_expand, pow_zero, mul_one]

Result:
no goals

Proof state:
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ (m + s))) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree

Tactic:
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand

Result:
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : g = (expand F (q ^ s)) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree

Proof state:
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
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 : g.Separable
hg' : g'.Separable
hm : m ≤ m'
⊢ g.natDegree = g'.natDegree

Tactic:
obtain ⟨s, rfl⟩ := exists_add_of_le hm

Result:
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ (m + s))) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree