R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ p % q = p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
⊢ p % q = p
have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
  not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ (divModByMonicAux p (_ : Monic (q * ↑C (leadingCoeff q)⁻¹))).snd = p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ p % q = p
rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ (if h : degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p ∧ p ≠ 0 then
        let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹));
        let_fun _wf :=
          (_ :
            degree
                (p -
                  ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) *
                    (q * ↑C (leadingCoeff q)⁻¹)) <
              degree p);
        let dm := divModByMonicAux (p - z * (q * ↑C (leadingCoeff q)⁻¹)) (_ : Monic (q * ↑C (leadingCoeff q)⁻¹));
        (z + dm.fst, dm.snd)
      else (0, p)).snd =
    p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ (divModByMonicAux p (_ : Monic (q * ↑C (leadingCoeff q)⁻¹))).snd = p
unfold divModByMonicAux
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ (if degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p ∧ ¬p = 0 then
        (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) +
            (divModByMonicAux
                (p -
                  ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) *
                    (q * ↑C (leadingCoeff q)⁻¹))
                (_ : Monic (q * ↑C (leadingCoeff q)⁻¹))).fst,
          (divModByMonicAux
              (p -
                ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) *
                  (q * ↑C (leadingCoeff q)⁻¹))
              (_ : Monic (q * ↑C (leadingCoeff q)⁻¹))).snd)
      else (0, p)).snd =
    p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ (if h : degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p ∧ p ≠ 0 then
        let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹));
        let_fun _wf :=
          (_ :
            degree
                (p -
                  ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) *
                    (q * ↑C (leadingCoeff q)⁻¹)) <
              degree p);
        let dm := divModByMonicAux (p - z * (q * ↑C (leadingCoeff q)⁻¹)) (_ : Monic (q * ↑C (leadingCoeff q)⁻¹));
        (z + dm.fst, dm.snd)
      else (0, p)).snd =
    p
dsimp
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
this : ¬degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
⊢ (if degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p ∧ ¬p = 0 then
        (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) +
            (divModByMonicAux
                (p -
                  ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) *
                    (q * ↑C (leadingCoeff q)⁻¹))
                (_ : Monic (q * ↑C (leadingCoeff q)⁻¹))).fst,
          (divModByMonicAux
              (p -
                ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree (q * ↑C (leadingCoeff q)⁻¹)) *
                  (q * ↑C (leadingCoeff q)⁻¹))
              (_ : Monic (q * ↑C (leadingCoeff q)⁻¹))).snd)
      else (0, p)).snd =
    p
simp only [this, false_and_iff, if_false]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
⊢ degree (q * ↑C (leadingCoeff q)⁻¹) > degree p
rwa [degree_mul_leadingCoeff_inv q hq0]