awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
a b : R
rw :
  (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).IsMonicOfDegree
    2
⊢ (HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).IsMonicOfDegree
    2

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
a b : R
⊢ max (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree
      (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) b)) =
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
a b : R
⊢ (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).IsMonicOfDegree
    2

Tactic:
exact (isMonicOfDegree_X_pow R 2).add_right <|
    calc
    _ ≤ max (C a * X).natDegree (C b).natDegree := natDegree_add_le ..
    _ = (C a * X).natDegree := by simp
    _ < 2 := natDegree_C_mul_le .. |>.trans natDegree_X_le |>.trans_lt one_lt_two

Premises used: Polynomial.C, Polynomial.natDegree_C_mul_le, Max.max, one_lt_two, Polynomial.natDegree_X_le, LE.le.trans, Polynomial.natDegree, OfNat.ofNat, Polynomial.IsMonicOfDegree.add_right, LE.le.trans_lt, DFunLike.coe, Polynomial.isMonicOfDegree_X_pow, Polynomial.natDegree_add_le
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
⊢ f.IsMonicOfDegree 2 ↔
    ∃ (a : R) (b : R),
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])

Tactic:
⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_add_add_two a b⟩

Premises used: Polynomial.isMonicOfDegree_add_add_two, Eq.rec, Iff.intro, _private.0.Polynomial.isMonicOfDegree_two_iff.match_1, Polynomial.IsMonicOfDegree, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
refine :
  ∀ (H : f.IsMonicOfDegree 2),
    ∃ (a : R) (b : R),
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])
⊢ f.IsMonicOfDegree 2 ↔
    ∃ (a : R) (b : R),
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_add_add_two a b⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ ∃ (a : R) (b : R),
    f =
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])

Tactic:
⟨f.coeff 1, f.coeff 0, ext fun n ↦ ?_⟩

Premises used: Polynomial.ext, Polynomial.coeff, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
refine :
  ∀ (n : ℕ),
    f.coeff n =
      (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
            ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
        n
⊢ ∃ (a : R) (b : R),
    f =
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])

Tactic:
refine ⟨f.coeff 1, f.coeff 0, ext fun n ↦ ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
inl :
  ∀ (hn : n < 1),
    f.coeff n =
      (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
            ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
        n
inr :
  f.coeff 1 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
      1
inr₁ :
  ∀ (hn : 1 < n),
    f.coeff n =
      (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
            ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
        n
⊢ f.coeff n =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
      n

Tactic:
rcases lt_trichotomy n 1 with hn | rfl | hn

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : n < 1
⊢ n = 0

Tactic:
Nat.lt_one_iff.mp hn

Premises used: Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : n < 1
inl :
  ∀ (hn : LT.lt (α := ℕ) 0 1),
    f.coeff 0 =
      (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
            ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
        0
⊢ f.coeff n =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
      n

Tactic:
obtain rfl : n = 0 := Nat.lt_one_iff.mp hn

Premises used: Nat.lt_one_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
hn : LT.lt (α := ℕ) 0 1
⊢ f.coeff 0 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
      0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ f.coeff 1 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
      1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ 2 ≤ n

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ f.coeff n =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (f.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff
      n

Tactic:
exact H.coeff_eq (isMonicOfDegree_add_add_two ..) (by lia)

Premises used: Polynomial.IsMonicOfDegree.coeff_eq, Polynomial.isMonicOfDegree_add_add_two
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
obtain :
  ∀ (q : R[X]) (hq₁ : p = HPow.hPow (α := R[X]) X n + q) (hq₂ : q.natDegree < n),
    (p - HPow.hPow (α := R[X]) X n).natDegree < n
⊢ (p - HPow.hPow (α := R[X]) X n).natDegree < n

Tactic:
obtain ⟨q, hq₁, hq₂⟩ := hp.exists_natDegree_lt hn

Premises used: Polynomial.IsMonicOfDegree.exists_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
q : R[X]
hq₁ : p = HPow.hPow (α := R[X]) X n + q
hq₂ : q.natDegree < n
⊢ (p - HPow.hPow (α := R[X]) X n).natDegree < n

Tactic:
simpa [hq₁]
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
rw : (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree < n
⊢ (p - q).natDegree < n

Tactic:
rw [← sub_sub_sub_cancel_right p q (X ^ n)]

Premises used: sub_sub_sub_cancel_right, HPow.hPow, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
⊢ (p - HPow.hPow (α := R[X]) X n).natDegree < n

Tactic:
replace hp := hp.natDegree_sub_X_pow hn
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hq : q.IsMonicOfDegree n
hp : (p - HPow.hPow (α := R[X]) X n).natDegree < n
⊢ (q - HPow.hPow (α := R[X]) X n).natDegree < n

Tactic:
replace hq := hq.natDegree_sub_X_pow hn
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : (p - HPow.hPow (α := R[X]) X n).natDegree < n
hq : (q - HPow.hPow (α := R[X]) X n).natDegree < n
rw :
  ∀ (hp : (p - HPow.hPow (α := R[X]) X n).natDegree ≤ n - 1) (hq : (q - HPow.hPow (α := R[X]) X n).natDegree ≤ n - 1),
    (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree ≤ n - 1
⊢ (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree < n

Tactic:
rw [← Nat.le_sub_one_iff_lt (Nat.zero_lt_of_ne_zero hn)] at hp hq ⊢

Premises used: Nat.le_sub_one_iff_lt, Nat.zero_lt_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : (p - HPow.hPow (α := R[X]) X n).natDegree ≤ n - 1
hq : (q - HPow.hPow (α := R[X]) X n).natDegree ≤ n - 1
⊢ (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree ≤ n - 1

Tactic:
(natDegree_sub_le_iff_left hq).mpr hp

Premises used: Iff.mpr, Polynomial.natDegree_sub_le_iff_left
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : (p - HPow.hPow (α := R[X]) X n).natDegree ≤ n - 1
hq : (q - HPow.hPow (α := R[X]) X n).natDegree ≤ n - 1
⊢ (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree ≤ n - 1

Tactic:
exact (natDegree_sub_le_iff_left hq).mpr hp

Premises used: Iff.mpr, Polynomial.natDegree_sub_le_iff_left
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p + -q).IsMonicOfDegree n

Tactic:
hp.add_right <| (natDegree_neg q) ▸ hq

Premises used: Eq.rec, Polynomial.natDegree_neg, Polynomial.IsMonicOfDegree.add_right, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p + -q).IsMonicOfDegree n

Tactic:
exact hp.add_right <| (natDegree_neg q) ▸ hq

Premises used: Polynomial.IsMonicOfDegree.add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
r : R
rw : LT.lt (α := ℕ) 0 1
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) < 1

Tactic:
rw [natDegree_C]

Premises used: Polynomial.natDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
r : R
⊢ LT.lt (α := ℕ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
r : R
⊢ LT.lt (α := ℕ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
rw :
  (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
        HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).IsMonicOfDegree
    2
⊢ (HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).IsMonicOfDegree
    2

Tactic:
rw [sub_add]

Premises used: sub_add
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
rw :
  (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree <
    2
⊢ (-HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).natDegree <
    2

Tactic:
rw [natDegree_neg]

Premises used: Polynomial.natDegree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
⊢ (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    max (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree
      (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) b))

Tactic:
natDegree_sub_le ..

Premises used: Polynomial.natDegree_sub_le
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
⊢ max (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree
      (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) b)) =
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree < 2

Tactic:
natDegree_C_mul_le .. |>.trans natDegree_X_le |>.trans_lt one_lt_two

Premises used: Polynomial.natDegree_C_mul_le, one_lt_two, Polynomial.natDegree_X_le, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
_ :
  max (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree
      (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) b)) =
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree
⊢ (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree <
    2

Tactic:
calc
    _ ≤ max (C a * X).natDegree (C b).natDegree := natDegree_sub_le ..
    _ = (C a * X).natDegree := by simp
    _ < 2 := natDegree_C_mul_le .. |>.trans natDegree_X_le |>.trans_lt one_lt_two

Premises used: Polynomial.C, Polynomial.natDegree_C_mul_le, Max.max, one_lt_two, Polynomial.natDegree_X_le, LE.le.trans, Polynomial.natDegree, LE.le.trans_lt, DFunLike.coe, Polynomial.natDegree_sub_le
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
⊢ (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
        HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).IsMonicOfDegree
    2

Tactic:
exact (isMonicOfDegree_X_pow R 2).add_right <| by
    rw [natDegree_neg]
    calc
    _ ≤ max (C a * X).natDegree (C b).natDegree := natDegree_sub_le ..
    _ = (C a * X).natDegree := by simp
    _ < 2 := natDegree_C_mul_le .. |>.trans natDegree_X_le |>.trans_lt one_lt_two

Premises used: OfNat.ofNat, Polynomial.IsMonicOfDegree.add_right, Polynomial.isMonicOfDegree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
f : R[X]
⊢ f.IsMonicOfDegree 2 ↔
    ∃ (a : R) (b : R),
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])

Tactic:
⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_sub_add_two a b⟩

Premises used: _private.0.Polynomial.isMonicOfDegree_two_iff'.match_1, Eq.rec, Iff.intro, Polynomial.IsMonicOfDegree, OfNat.ofNat, Eq.symm, Polynomial.isMonicOfDegree_sub_add_two
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
f : R[X]
refine :
  ∀ (H : f.IsMonicOfDegree 2),
    ∃ (a : R) (b : R),
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])
⊢ f.IsMonicOfDegree 2 ↔
    ∃ (a : R) (b : R),
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_sub_add_two a b⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
simp :
  ∃ (a : R) (b : R),
    f =
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (-a) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])
⊢ ∃ (a : R) (b : R),
    f =
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])

Tactic:
simp only [sub_eq_add_neg, ← neg_mul, ← map_neg]

Premises used: sub_eq_add_neg, map_neg, neg_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
obtain :
  ∀ (a b : R)
    (h :
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])),
    ∃ (a : R) (b : R),
      f =
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (-a) : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])
⊢ ∃ (a : R) (b : R),
    f =
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (-a) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])

Tactic:
obtain ⟨a, b, h⟩ := isMonicOfDegree_two_iff.mp H

Premises used: Polynomial.isMonicOfDegree_two_iff, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
a b : R
h :
  f =
    HAdd.hAdd (β := R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])
⊢ ∃ (a : R) (b : R),
    f =
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (-a) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])

Tactic:
⟨-a, b, (neg_neg a).symm ▸ h⟩

Premises used: Eq.rec, neg_neg, Exists.intro, Eq.symm, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
a b : R
h :
  f =
    HAdd.hAdd (β := R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])
⊢ ∃ (a : R) (b : R),
    f =
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (-a) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])

Tactic:
exact ⟨-a, b, (neg_neg a).symm ▸ h⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
obtain : ∀ (q : R[X]) (hq : a + r = q * b), ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b - r
⊢ ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b - r

Tactic:
obtain ⟨q, hq⟩ := exists_eq_mul_left_of_dvd h

Premises used: exists_eq_mul_left_of_dvd
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b - r

Tactic:
⟨q, hb.of_mul_right ?_, eq_sub_iff_add_eq.mpr hq⟩

Premises used: Iff.mpr, Polynomial.IsMonicOfDegree.of_mul_right, eq_sub_iff_add_eq, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
refine : (q * b).IsMonicOfDegree (m - n + n)
⊢ ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b - r

Tactic:
refine ⟨q, hb.of_mul_right ?_, eq_sub_iff_add_eq.mpr hq⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ m - n + n = m

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
rw : (a + r).IsMonicOfDegree m
⊢ (q * b).IsMonicOfDegree (m - n + n)

Tactic:
rw [← hq, show m - n + n = m by lia]
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ (a + r).IsMonicOfDegree m

Tactic:
ha.add_right hr

Premises used: Polynomial.IsMonicOfDegree.add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ (a + r).IsMonicOfDegree m

Tactic:
exact ha.add_right hr

Premises used: Polynomial.IsMonicOfDegree.add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
⊢ ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b - -r

Tactic:
ha.of_dvd_add hmn hb ?_ h

Premises used: Polynomial.IsMonicOfDegree.of_dvd_add