awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
⊢ f.IsMonicOfDegree 1 ↔ ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])
have refine : ∀ (H : f.IsMonicOfDegree 1), ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])
Tactic: refine ⟨fun H ↦ ?_, fun ⟨r, H⟩ ↦ H ▸ isMonicOfDegree_X_add_one r⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
⊢ ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])
have refine : f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
Tactic: refine ⟨f.coeff 0, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
⊢ f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
have a : ∀ (n : ℕ), f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
n : ℕ
⊢ f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n
have a : f.coeff 0 = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff 0
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
n : ℕ
a : f.coeff 0 = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff 0
⊢ f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n
have a₁ : ∀ (hn : n > 0), f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
a b : R
⊢ (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
have 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
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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])
have 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])
Tactic: refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_add_add_two a b⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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])
have 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
Tactic: refine ⟨f.coeff 1, f.coeff 0, ext fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
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
have 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
Tactic: rcases lt_trichotomy n 1 with hn | rfl | hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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
⊢ 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
have 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
Tactic: rcases lt_trichotomy n 1 with hn | rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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
⊢ 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
have 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
Tactic: rcases lt_trichotomy n 1 with hn | rfl | hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
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
have 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
Tactic: obtain rfl : n = 0 := Nat.lt_one_iff.mp hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ (p - HPow.hPow (α := R[X]) X n).natDegree < n
have 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
Tactic: obtain ⟨q, hq₁, hq₂⟩ := hp.exists_natDegree_lt hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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 - q).natDegree < n
have rw : (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree < n
Tactic: rw [← sub_sub_sub_cancel_right p q (X ^ n)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
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 - (q - HPow.hPow (α := R[X]) X n)).natDegree < n
have hp₁ : (p - HPow.hPow (α := R[X]) X n).natDegree < n
Tactic: replace hp := hp.natDegree_sub_X_pow hn
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
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
⊢ (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree < n
have hq₁ : (q - HPow.hPow (α := R[X]) X n).natDegree < n
Tactic: replace hq := hq.natDegree_sub_X_pow hn
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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
⊢ (p - HPow.hPow (α := R[X]) X n - (q - HPow.hPow (α := R[X]) X n)).natDegree < n
have 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
Tactic: rw [← Nat.le_sub_one_iff_lt (Nat.zero_lt_of_ne_zero hn)] at hp hq ⊢
Cleared hypotheses: hp, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
r : R
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) < 1
have rw : LT.lt (α := ℕ) 0 1
Tactic: rw [natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
a b : R
⊢ (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
have 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
Tactic: rw [sub_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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 <
    2
have 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
Tactic: rw [natDegree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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 <
    2
have _ : 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: 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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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])
have 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])
Tactic: refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_sub_add_two a b⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Ring 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])
have 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])
Tactic: simp only [sub_eq_add_neg, ← neg_mul, ← map_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Ring 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])
have 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])
Tactic: obtain ⟨a, b, h⟩ := isMonicOfDegree_two_iff.mp H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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
have obtain : ∀ (q : R[X]) (hq : a + r = q * b), ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b - r
Tactic: obtain ⟨q, hq⟩ := exists_eq_mul_left_of_dvd h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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
have refine : (q * b).IsMonicOfDegree (m - n + n)
Tactic: refine ⟨q, hb.of_mul_right ?_, eq_sub_iff_add_eq.mpr hq⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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 * b).IsMonicOfDegree (m - n + n)
have rw : (a + r).IsMonicOfDegree m
Tactic: rw [← hq, show m - n + n = m by lia]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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
have h₁ : ∀ (q : R[X]), q * b + r = q * b - -r
Tactic: convert! ha.of_dvd_add hmn hb ?_ h using 4 with q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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
h₁ : ∀ (q : R[X]), q * b + r = q * b - -r
⊢ ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b + r
have convert! : (-r).natDegree < m
Tactic: convert! ha.of_dvd_add hmn hb ?_ h using 4 with q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
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 * b + r = q * b - -r
have h₁ : q * b + r = q * b + r
Tactic: rw [sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
have inl : ∀ (H : Subsingleton R),
  IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
Tactic: rcases subsingleton_or_nontrivial R with H | H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
inl :
  ∀ (H : Subsingleton R),
    IsMonicOfDegree.{u_1} (R := R)
      ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
have inr : ∀ (H : Nontrivial R),
  IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
Tactic: rcases subsingleton_or_nontrivial R with H | H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
have inr : IsMonicOfDegree.{u_1} (R := R)
  ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) (n * 1)
Tactic: rw [← mul_one n]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
have rw : IsMonicOfDegree.{u_1} (R := R)
  ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) : (a : R[X]) → R[X]) p) n
Tactic: rw [sub_eq_add_neg, ← map_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ (p.comp q).natDegree ≤ p.natDegree * q.natDegree
have rw : 0 ≤ p.natDegree * q.natDegree
Tactic: rw [h0, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) + n • q.degree ≤
    (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
      HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ)
have grw : (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
    HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ) ≤
  (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
    HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ)
Tactic: grw [degree_le_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
      HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ) =
    (↑(n * q.natDegree) : WithBot ℕ)
have rw : HMul.hMul (α := WithBot ℕ) (↑n : WithBot ℕ) (↑q.natDegree : WithBot ℕ) = (↑(n * q.natDegree) : WithBot ℕ)
Tactic: rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ LE.le (α := ℕ) (↑(n * q.natDegree) : ℕ) (↑(p.natDegree * q.natDegree) : ℕ)
have a : n ≤ p.natDegree
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos : ∀ (hq : q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
Tactic: by_cases hq : natDegree q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
pos : ∀ (hq : q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have neg : ∀ (hq : ¬q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
Tactic: by_cases hq : natDegree q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have neg : (p.comp q).coeff (p.natDegree * q.natDegree) ≠ 0
Tactic: apply natDegree_eq_of_le_of_coeff_ne_zero natDegree_comp_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
⊢ False
have this : p = (C : (a : R) → R[X]) (p.coeff 0)
Tactic: have := eq_C_of_degree_le_zero hlt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
this : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ False
have h₁ : p.coeff 0 = 0
Tactic: rw [IsRoot, this, eval_C] at h
Cleared hypotheses: h, hlt, this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ False
have this₁ : p = 0
Tactic: simp only [h, map_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
⊢ p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
have simp_rw : p.degree ≤ (↑n : WithBot ℕ) ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
Tactic: simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
simp_rw : p.degree ≤ (↑n : WithBot ℕ) ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
⊢ p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
have simp_rw₁ : (∀ (m : ℕ), LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑m : WithBot ℕ) → p.coeff m = 0) ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
Tactic: simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_lt]