-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem degree_divX_lt (hp0 : p ≠ 0) : (divX p).degree < p.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ ⊥ < (C ((C (p.coeff 0)).coeff 0)).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 ≤ p.divX.degree

Tactic:
rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ¬p = C (p.coeff 0)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 + X.degree ≤ p.divX.degree + X.degree

Tactic:
exact add_le_add
  (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
      exact fun h0 => h (h0.symm ▸ degree_C_le))
      le_rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ ¬C ((C (p.coeff 0)).coeff 0) = 0

Tactic:
simpa using h'

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ¬p = C (p.coeff 0)

Tactic:
exact fun h0 => h (h0.symm ▸ degree_C_le)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
have hXp0 : divX p ≠ 0 := by
  simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ p.divX.degree < p.degree

Tactic:
calc
  degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
    if h : degree p ≤ 0 then by
      have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
      rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
      exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
    else by
      have hXp0 : divX p ≠ 0 := by
        simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
      have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
      have : degree (C (p.coeff 0)) < degree (divX p * X) :=
        calc
          degree (C (p.coeff 0)) ≤ 0 := degree_C_le
          _ < 1 := by decide
          _ = degree (X : R[X]) := degree_X.symm
          _ ≤ degree (divX p * X) := by
            rw [← zero_add (degree X), degree_mul' this]
            exact add_le_add
              (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                  exact fun h0 => h (h0.symm ▸ degree_C_le))
                  le_rfl
      rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
  _ = degree p := congr_arg _ (divX_mul_X_add _)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree

Tactic:
exact degree_lt_degree_mul_X hXp0

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX ≠ 0

Tactic:
simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
have : degree (C (p.coeff 0)) < degree (divX p * X) :=
  calc
    degree (C (p.coeff 0)) ≤ 0 := degree_C_le
    _ < 1 := by decide
    _ = degree (X : R[X]) := degree_X.symm
    _ ≤ degree (divX p * X) := by
      rw [← zero_add (degree X), degree_mul' this]
      exact add_le_add
        (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
            exact fun h0 => h (h0.symm ▸ degree_C_le))
            le_rfl

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ ⊥ < (C ((C (p.coeff 0)).coeff 0)).degree

Tactic:
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt this]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
⊢ p.divX.leadingCoeff * X.leadingCoeff ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ X.degree ≤ (p.divX * X).degree

Tactic:
rw [← zero_add (degree X), degree_mul' this]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 + X.degree ≤ p.divX.degree + X.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
⊢ p.divX.degree < p.degree

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ p.divX.degree < p.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ C (p.coeff 0) ≠ 0

Tactic:
rwa [← eq_C_of_degree_le_zero h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree