-- Mathlib/Algebra/Polynomial/FieldDivision.lean
lemma natDegree_mod_lt [Field k] (p : k[X]) {q : k[X]} (hq : q.natDegree ≠ 0) :
    (p % q).natDegree < q.natDegree

Proof state:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ (p % q).natDegree < q.natDegree

Tactic:
have hq' : q.leadingCoeff ≠ 0 := by
  rw [leadingCoeff_ne_zero]
  contrapose! hq
  simp [hq]

Result:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p % q).natDegree < q.natDegree

Proof state:
case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q * C q.leadingCoeff⁻¹ ≠ 1

Tactic:
contrapose! hq

Result:
case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : q * C q.leadingCoeff⁻¹ = 1
⊢ q.natDegree = 0

Proof state:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q.leadingCoeff ≠ 0

Tactic:
rw [leadingCoeff_ne_zero]

Result:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q ≠ 0

Proof state:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q ≠ 0

Tactic:
contrapose! hq

Result:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q = 0
⊢ q.natDegree = 0

Proof state:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p % q).natDegree < q.natDegree

Tactic:
rw [mod_def]

Result:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p %ₘ (q * C q.leadingCoeff⁻¹)).natDegree < q.natDegree

Proof state:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q = 0
⊢ q.natDegree = 0

Tactic:
simp [hq]

Result:
no goals

Proof state:
case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q.leadingCoeff * q.leadingCoeff⁻¹ = 1

Tactic:
rw [mul_inv_eq_one₀ hq']

Result:
no goals

Proof state:
case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : q * C q.leadingCoeff⁻¹ = 1
⊢ (q * C q.leadingCoeff⁻¹).natDegree = 0

Tactic:
simp [hq]

Result:
no goals

Proof state:
case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Result:
case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q.leadingCoeff * q.leadingCoeff⁻¹ = 1

Proof state:
case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : q * C q.leadingCoeff⁻¹ = 1
⊢ q.natDegree = 0

Tactic:
rw [← natDegree_mul_C_eq_of_mul_eq_one ((inv_mul_eq_one₀ hq').mpr rfl)]

Result:
case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : q * C q.leadingCoeff⁻¹ = 1
⊢ (q * C q.leadingCoeff⁻¹).natDegree = 0

Proof state:
case refine_3
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).natDegree ≤ q.natDegree

Tactic:
exact natDegree_mul_C_le q q.leadingCoeff⁻¹

Result:
no goals

Proof state:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p %ₘ (q * C q.leadingCoeff⁻¹)).natDegree < q.natDegree

Tactic:
refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_

Result:
case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).Monic

case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q * C q.leadingCoeff⁻¹ ≠ 1

case refine_3
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).natDegree ≤ q.natDegree