R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
⊢ degree (p %ₘ q) < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
⊢ degree (p %ₘ q) < degree q
have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q) < degree q
⊢ degree (p %ₘ q) < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
⊢ degree (p %ₘ q) < degree q
have :
  degree ((p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q) < degree q :=
  degree_modByMonic_lt (p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree (if hq : Monic q then (divModByMonicAux p hq).snd else p) < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q) < degree q
⊢ degree (p %ₘ q) < degree q
unfold modByMonic at this ⊢
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).snd
      else p) <
    degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree (if hq : Monic q then (divModByMonicAux p hq).snd else p) < degree q
unfold divModByMonicAux
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree
      (if h : Monic q then
        (if degree q ≤ degree p ∧ ¬p = 0 then
            (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
          else (0, p)).snd
      else p) <
    degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).snd
      else p) <
    degree q
dsimp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd < degree q
⊢ degree
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).snd <
    degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree
      (if h : Monic q then
        (if degree q ≤ degree p ∧ ¬p = 0 then
            (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
          else (0, p)).snd
      else p) <
    degree q
rw [dif_pos hq] at this ⊢
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd < degree q
⊢ degree
      (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
          (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd).snd <
    degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd < degree q
⊢ degree
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).snd <
    degree q
rw [if_pos h]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd < degree q
⊢ degree
      (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
          (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd).snd <
    degree q
exact this
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p →
    degree
        (if h : Monic q then
          (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
              let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
              let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
              let dm := divModByMonicAux (p - z * q) (_ : Monic q);
              (z + dm.fst, dm.snd)
            else (0, p)).snd
        else p) <
      degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p → degree (p %ₘ q) < degree q
unfold modByMonic divModByMonicAux
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p →
    degree
        (if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).snd
        else p) <
      degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p →
    degree
        (if h : Monic q then
          (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
              let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
              let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
              let dm := divModByMonicAux (p - z * q) (_ : Monic q);
              (z + dm.fst, dm.snd)
            else (0, p)).snd
        else p) <
      degree q
dsimp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p → degree (0, p).snd < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p →
    degree
        (if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).snd
        else p) <
      degree q
rw [dif_pos hq, if_neg h]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p → degree (0, p).snd < degree q
exact lt_of_not_ge
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree (p %ₘ q) < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬p ≠ 0 → degree (p %ₘ q) < degree q
intro hp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).snd
      else p) <
    degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree (p %ₘ q) < degree q
unfold modByMonic divModByMonicAux
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree
      (if h : Monic q then
        (if degree q ≤ degree p ∧ ¬p = 0 then
            (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
          else (0, p)).snd
      else p) <
    degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).snd
      else p) <
    degree q
dsimp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree (0, 0).snd < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree
      (if h : Monic q then
        (if degree q ≤ degree p ∧ ¬p = 0 then
            (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
          else (0, p)).snd
      else p) <
    degree q
rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree (0, 0).snd < degree q
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero))