R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
nontriviality R
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g

case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
by_cases hfg : f /ₘ g = 0
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
have hgf := hfg
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬degree f < degree g
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
rw [divByMonic_eq_zero_iff hg] at hgf
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬degree f < degree g
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
push_neg  at hgf
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
have := degree_add_divByMonic hg hgf
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f ≠ 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
have hf : f ≠ 0 := by
  intro hf
  apply hfg
  rw [hf, zero_divByMonic]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : natDegree g + natDegree (f /ₘ g) = natDegree f
hf : f ≠ 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f ≠ 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
  Nat.cast_withBot, Nat.cast_withBot, Nat.cast_withBot,
  ← WithBot.coe_add, WithBot.coe_eq_coe] at this
no goals
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : natDegree g + natDegree (f /ₘ g) = natDegree f
hf : f ≠ 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
rw [← this, add_tsub_cancel_left]
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = natDegree f - natDegree g
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
rw [hfg, natDegree_zero]
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : degree f < degree g
⊢ 0 = natDegree f - natDegree g
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = natDegree f - natDegree g
rw [divByMonic_eq_zero_iff hg] at hfg
no goals
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : degree f < degree g
⊢ 0 = natDegree f - natDegree g
rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f = 0
⊢ False
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
⊢ f ≠ 0
intro hf
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f = 0
⊢ f /ₘ g = 0
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f = 0
⊢ False
apply hfg
no goals
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f = 0
⊢ f /ₘ g = 0
rw [hf, zero_divByMonic]