-- Mathlib/RingTheory/Polynomial/Wronskian.lean
theorem natDegree_wronskian_lt_add {a b : R[X]} (hw : wronskian a b ≠ 0) :
    (wronskian a b).natDegree < a.natDegree + b.natDegree

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
⊢ b ≠ 0

Tactic:
intro h

Result:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
h : b = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ ↑(a.wronskian b).natDegree < ↑a.natDegree + ↑b.natDegree

Tactic:
convert ← degree_wronskian_lt_add ha hb

Result:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree = ↑(a.wronskian b).natDegree

case h.e'_4.h.e'_5
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree = ↑a.natDegree

case h.e'_4.h.e'_6
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree = ↑b.natDegree

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
h : a = 0
⊢ False

Tactic:
subst h

Result:
R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : wronskian 0 b ≠ 0
⊢ False

Proof state:
case h.e'_4.h.e'_5
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree = ↑a.natDegree

Tactic:
exact Polynomial.degree_eq_natDegree ha

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree = ↑(a.wronskian b).natDegree

Tactic:
exact Polynomial.degree_eq_natDegree hw

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R[X]
ha : a ≠ 0
hw : a.wronskian 0 ≠ 0
⊢ False

Tactic:
rw [wronskian_zero_right] at hw

Result:
R : Type u_1
inst✝ : CommRing R
a : R[X]
ha : a ≠ 0
hw : 0 ≠ 0
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
h : b = 0
⊢ False

Tactic:
subst h

Result:
R : Type u_1
inst✝ : CommRing R
a : R[X]
ha : a ≠ 0
hw : a.wronskian 0 ≠ 0
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
⊢ a ≠ 0

Tactic:
intro h

Result:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
h : a = 0
⊢ False

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

Tactic:
rw [← WithBot.coe_lt_coe, WithBot.coe_add]

Result:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ ↑(a.wronskian b).natDegree < ↑a.natDegree + ↑b.natDegree

Proof state:
R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : 0 ≠ 0
⊢ False

Tactic:
exact hw rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : wronskian 0 b ≠ 0
⊢ False

Tactic:
rw [wronskian_zero_left] at hw

Result:
R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : 0 ≠ 0
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Tactic:
have ha : a ≠ 0 := by intro h; subst h; rw [wronskian_zero_left] at hw; exact hw rfl

Result:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Proof state:
case h.e'_4.h.e'_6
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree = ↑b.natDegree

Tactic:
exact Polynomial.degree_eq_natDegree hb

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R[X]
ha : a ≠ 0
hw : 0 ≠ 0
⊢ False

Tactic:
exact hw rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Tactic:
have hb : b ≠ 0 := by intro h; subst h; rw [wronskian_zero_right] at hw; exact hw rfl

Result:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree