-- Mathlib/Algebra/Polynomial/Div.lean
theorem natDegree_divByMonic (f : R[X]) {g : R[X]} (hg : g.Monic) :
    natDegree (f /ₘ g) = natDegree f - natDegree g

Proof state:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [hfg, natDegree_zero]

Result:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree

Proof state:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
  ← Nat.cast_add, Nat.cast_inj] at this

Result:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Proof state:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ False

Tactic:
apply hfg

Result:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ f /ₘ g = 0

Proof state:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
⊢ f ≠ 0

Tactic:
intro hf

Result:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ False

Proof state:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
have := degree_add_divByMonic hg hgf

Result:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Proof state:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ f /ₘ g = 0

Tactic:
rw [hf, zero_divByMonic]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = f.natDegree - g.natDegree

Tactic:
rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree

Tactic:
rw [divByMonic_eq_zero_iff hg] at hfg

Result:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = f.natDegree - g.natDegree

Proof state:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [divByMonic_eq_zero_iff hg] at hgf

Result:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬f.degree < g.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Proof state:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
have hgf := hfg

Result:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Proof state:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
by_cases hfg : f /ₘ g = 0

Result:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Proof state:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Proof state:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
have hf : f ≠ 0 := by
  intro hf
  apply hfg
  rw [hf, zero_divByMonic]

Result:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Proof state:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [← this, add_tsub_cancel_left]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬f.degree < g.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
push_neg at hgf

Result:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree