-- Mathlib/RingTheory/Polynomial/Wronskian.lean
theorem degree_wronskian_lt_add {a b : R[X]} (ha : a ≠ 0) (hb : b ≠ 0) :
    (wronskian a b).degree < a.degree + b.degree

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree < a.degree + b.degree

Tactic:
apply lt_of_le_of_lt

Result:
case hab
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree ≤ ?b

case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ ?b < a.degree + b.degree

case b
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ WithBot ℕ

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree ⊔ (derivative a * b).degree < a.degree + b.degree

Tactic:
rw [max_lt_iff]

Result:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree < a.degree + b.degree ∧ (derivative a * b).degree < a.degree + b.degree

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a * b).degree < a.degree + b.degree

Tactic:
apply lt_of_le_of_lt

Result:
case hab
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a * b).degree ≤ ?b

case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ ?b < a.degree + b.degree

case b
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ WithBot ℕ

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree < a.degree + b.degree ∧ (derivative a * b).degree < a.degree + b.degree

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree < a.degree + b.degree

case right
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a * b).degree < a.degree + b.degree

Proof state:
case hab
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree ≤ ?b

Tactic:
exact degree_mul_le a (derivative b)

Result:
no goals

Proof state:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree

Tactic:
rw [← Polynomial.degree_ne_bot] at ha

Result:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree

Proof state:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a).degree + b.degree < a.degree + b.degree

Tactic:
rw [← Polynomial.degree_ne_bot] at hb

Result:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree + b.degree < a.degree + b.degree

Proof state:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ (derivative b).degree < b.degree

Tactic:
exact Polynomial.degree_derivative_lt hb

Result:
no goals

Proof state:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree + b.degree < a.degree + b.degree

Tactic:
rw [WithBot.add_lt_add_iff_right hb]

Result:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree < a.degree

Proof state:
case hab
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a * b).degree ≤ ?b

Tactic:
exact degree_mul_le (derivative a) b

Result:
no goals

Proof state:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree < a.degree

Tactic:
exact Polynomial.degree_derivative_lt ha

Result:
no goals

Proof state:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree

Tactic:
rw [WithBot.add_lt_add_iff_left ha]

Result:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ (derivative b).degree < b.degree