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
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
let ⟨a, ha⟩ := hf.dvd_degree'
no goals
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
rw [← ha, one_pow a, mul_one]