awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
hda : (a * b).natDegree = 2
⊢ ∃ (c₁ : R) (c₂ : R), (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂
have hda₁ : a.natDegree + 1 = 2
Tactic: rw [ha.natDegree_mul hb, hdb] at hda
Cleared hypotheses: hda
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
hda : a.natDegree + 1 = 2
⊢ ∃ (c₁ : R) (c₂ : R), (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂
have right : (a * b).coeff 1 = a.coeff 0 + b.coeff 0
Tactic: use a.coeff 0, b.coeff 0, mul_coeff_zero a b
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ ∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)
have inr : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
  p
Tactic: refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
inr :
  HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
      HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
    p
⊢ ∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)
have inr₁ : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X])).natDegree ∈ Ioc 0 (2 / 2)
Tactic: refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
      HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
    p
have inr : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c₁ : R[X]) ((C : (a : R) → R[X]) c₂ : R[X]) *
        HPow.hPow (α := R[X]) (β := ℕ) X 0 +
      HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c₁ : R[X]) ((C : (a : R) → R[X]) c₂ : R[X]) *
        HPow.hPow (α := R[X]) (β := ℕ) X 1 +
    1 * HPow.hPow (α := R[X]) (β := ℕ) X 2
Tactic: rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
          Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).natDegree = P.natDegree
have refine : (Polynomial.map f P).coeff P.natDegree ≠ 0
Tactic: refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0
have rw : Ne.{v + 1} (α := S) 1 0
Tactic: rw [coeff_map, Monic.coeff_natDegree hmo, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
hp : (map f p).Monic
⊢ p.Monic
have a : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) ((f : (a : R) → S) 1 : S)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
hp : (map f p).Monic
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) ((f : (a : R) → S) 1 : S)
have a : (map f p).leadingCoeff = (f : (a : R) → S) 1
Tactic: rw [← leadingCoeff_map_of_injective hf, hp.leadingCoeff, f.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
hp : (map f p).Monic
a : (map f p).leadingCoeff = (f : (a : R) → S) 1
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) ((f : (a : R) → S) 1 : S)
have a₁ : Eq.{v + 1} (α := S) (1 : S) ((f : (a : R) → S) 1 : S)
Tactic: rw [← leadingCoeff_map_of_injective hf, hp.leadingCoeff, f.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
hp : (map f p).Monic
a : (map f p).leadingCoeff = (f : (a : R) → S) 1
a₁ : Eq.{v + 1} (α := S) (1 : S) ((f : (a : R) → S) 1 : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) ((f : (a : R) → S) 1 : S)
have a₂ : Eq.{v + 1} (α := S) 1 1
Tactic: rw [← leadingCoeff_map_of_injective hf, hp.leadingCoeff, f.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
⊢ (-p).degree < (↑n : WithBot ℕ)
have rwa : ∀ (H : (-p).degree < (↑n : WithBot ℕ)), (-p).degree < (↑n : WithBot ℕ)
Tactic: rwa [← degree_neg p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
⊢ False
have inl : ∀ (h : IsUnit (HPow.hPow (α := R[X]) (β := ℕ) X 0 - 1)), False
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
inl : ∀ (h : IsUnit (HPow.hPow (α := R[X]) (β := ℕ) X 0 - 1)), False
⊢ False
have inr : ∀ (hn : n ≠ 0), False
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
hn : n ≠ 0
⊢ False
have inr : n = 0
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
hn : n ≠ 0
⊢ n = 0
have inr : n = natDegree.{u_1} (R := R) 1
Tactic: rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
hn : n ≠ 0
inr : n = natDegree.{u_1} (R := R) 1
⊢ n = 0
have inr₁ : n = (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).natDegree
Tactic: rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
hn : n ≠ 0
inr : n = natDegree.{u_1} (R := R) 1
inr₁ : n = (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).natDegree
⊢ n = 0
have inr₂ : n = n
Tactic: rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + -q).Monic
have apply : (-q).degree < p.degree
Tactic: apply hp.add_of_left
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (-q).coeff (-q).natDegree = 1
have rw : (-q).coeff q.natDegree = 1
Tactic: rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
rw : (-q).coeff q.natDegree = 1
⊢ (-q).coeff (-q).natDegree = 1
have rw₁ : -q.coeff q.natDegree = 1
Tactic: rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
rw : (-q).coeff q.natDegree = 1
rw₁ : -q.coeff q.natDegree = 1
⊢ (-q).coeff (-q).natDegree = 1
have rw₂ : Eq.{u + 1} (α := R) (- -1) 1
Tactic: rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
rw : (-q).coeff q.natDegree = 1
rw₁ : -q.coeff q.natDegree = 1
rw₂ : Eq.{u + 1} (α := R) (- -1) 1
⊢ (-q).coeff (-q).natDegree = 1
have rw₃ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (p - q).Monic
have this : (-q).coeff (-q).natDegree = 1
Tactic: have : (-q).coeff (-q).natDegree = 1 := by
    rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ (p + -q).Monic
have apply : p.degree < (-q).degree
Tactic: apply Monic.add_of_right this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
⊢ q * p ≠ 0
have pos : ∀ (h : p = 1), q * p ≠ 0
Tactic: by_cases h : p = 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
pos : ∀ (h : p = 1), q * p ≠ 0
⊢ q * p ≠ 0
have neg : ∀ (h : ¬p = 1), q * p ≠ 0
Tactic: by_cases h : p = 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0
have neg : ¬q = 0 ∧ ¬p.degree = ⊥
Tactic: rw [Ne, ← degree_eq_bot, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬p.degree = ⊥
have neg : ¬p.degree = ⊥
Tactic: refine ⟨hq, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬p.degree = ⊥
have h₁ : 0 < p.degree
Tactic: rw [← hp.degree_le_zero_iff_eq_one, not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ¬p.degree = ⊥
have neg : LT.lt (α := WithBot ℕ) ⊥ 0
Tactic: refine (lt_trans ?_ h).ne'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
⊢ p * q ≠ 0
have pos : ∀ (h : p = 1), p * q ≠ 0
Tactic: by_cases h : p = 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
pos : ∀ (h : p = 1), p * q ≠ 0
⊢ p * q ≠ 0
have neg : ∀ (h : ¬p = 1), p * q ≠ 0
Tactic: by_cases h : p = 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0
have neg : ¬q = 0 ∧ ¬p.degree = ⊥
Tactic: rw [Ne, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or,
    degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
have pos : ∀ (hq : q = 0), (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
pos : ∀ (hq : q = 0), (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
have neg : ∀ (hq : ¬q = 0), (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
have pos : 0 < p.natDegree ↔ p.natDegree ≠ 0
Tactic: suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simp [hq, ← h.natDegree_eq_zero, iffComm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ p * q = 0 ↔ q = 0
have pos : ∀ (hq : q = 0), p * q = 0 ↔ q = 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
pos : ∀ (hq : q = 0), p * q = 0 ↔ q = 0
⊢ p * q = 0 ↔ q = 0
have neg : ∀ (hq : ¬q = 0), p * q = 0 ↔ q = 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ q * p = 0 ↔ q = 0
have pos : ∀ (hq : q = 0), q * p = 0 ↔ q = 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
pos : ∀ (hq : q = 0), q * p = 0 ↔ q = 0
⊢ q * p = 0 ↔ q = 0
have neg : ∀ (hq : ¬q = 0), q * p = 0 ↔ q = 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
⊢ IsRegular p
have left : IsLeftRegular p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
left : IsLeftRegular p
⊢ IsRegular p
have right : IsRightRegular p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
⊢ q = r
have left : q - r = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
left : q - r = 0
⊢ q = r
have left₁ : p * (q - r) = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
left : q - r = 0
left₁ : p * (q - r) = 0
⊢ q = r
have left₂ : p * q - p * r = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
left : q - r = 0
left₁ : p * (q - r) = 0
left₂ : p * q - p * r = 0
⊢ q = r
have left₃ : p * r - p * r = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
left : q - r = 0
left₁ : p * (q - r) = 0
left₂ : p * q - p * r = 0
left₃ : p * r - p * r = 0
⊢ q = r
have left₄ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
⊢ q = r
have right : q - r = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
right : q - r = 0
⊢ q = r
have right₁ : (q - r) * p = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
right : q - r = 0
right₁ : (q - r) * p = 0
⊢ q = r
have right₂ : q * p - r * p = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
right : q - r = 0
right₁ : (q - r) * p = 0
right₂ : q * p - r * p = 0
⊢ q = r
have right₃ : r * p - r * p = 0
Tactic: rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
right : q - r = 0
right₁ : (q - r) * p = 0
right₂ : q * p - r * p = 0
right₃ : r * p - r * p = 0
⊢ q = r
have right₄ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree = p.degree
have refine_1 : (k • p).degree ≤ p.degree
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
refine_1 : (k • p).degree ≤ p.degree
⊢ (k • p).degree = p.degree
have refine_2 : p.degree ≤ (k • p).degree
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree ≤ p.degree
have refine_1 : ∀ (m : ℕ), p.degree < (↑m : WithBot ℕ) → (k • p).coeff m = 0
Tactic: rw [degree_le_iff_coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : p.degree < (↑m : WithBot ℕ)
⊢ (k • p).coeff m = 0
have hm₁ : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
Tactic: rw [degree_lt_iff_coeff_zero] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ p.degree ≤ (k • p).degree
have refine_2 : ∀ (m : ℕ), (k • p).degree < (↑m : WithBot ℕ) → p.coeff m = 0
Tactic: rw [degree_le_iff_coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : (k • p).degree < (↑m : WithBot ℕ)
⊢ p.coeff m = 0
have hm₁ : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
Tactic: rw [degree_lt_iff_coeff_zero] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ p.coeff m = 0
have refine_2 : Eq.{u + 1} (α := R) ((fun (x : R) ↦ k • x) (p.coeff m)) ((fun (x : R) ↦ k • x) 0)
Tactic: refine h ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).natDegree = p.natDegree
have pos : ∀ (hp : p = 0), (k • p).natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
pos : ∀ (hp : p = 0), (k • p).natDegree = p.natDegree
⊢ (k • p).natDegree = p.natDegree
have neg : ∀ (hp : ¬p = 0), (k • p).natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ (k • p).natDegree = p.natDegree
have neg : k • p ≠ 0
Tactic: rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hp, ← degree_eq_natDegree,
    degree_smul_of_smul_regular p h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0
have neg : ∀ (hp : k • p = 0), p = 0
Tactic: contrapose hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ p = 0
have hp₁ : k • p = HSMul.hSMul (β := R[X]) k 0
Tactic: rw [← smul_zero k] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).leadingCoeff = k • p.leadingCoeff
have rw : (k • p).coeff (k • p).natDegree = k • p.leadingCoeff
Tactic: rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
    natDegree_smul_of_smul_regular p h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
rw : (k • p).coeff (k • p).natDegree = k • p.leadingCoeff
⊢ (k • p).leadingCoeff = k • p.leadingCoeff
have rw₁ : (k • p).coeff (k • p).natDegree = k • p.coeff p.natDegree
Tactic: rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
    natDegree_smul_of_smul_regular p h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
rw : (k • p).coeff (k • p).natDegree = k • p.leadingCoeff
rw₁ : (k • p).coeff (k • p).natDegree = k • p.coeff p.natDegree
⊢ (k • p).leadingCoeff = k • p.leadingCoeff
have rw₂ : k • p.coeff (k • p).natDegree = k • p.coeff p.natDegree
Tactic: rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
    natDegree_smul_of_smul_regular p h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
rw : (k • p).coeff (k • p).natDegree = k • p.leadingCoeff
rw₁ : (k • p).coeff (k • p).natDegree = k • p.coeff p.natDegree
rw₂ : k • p.coeff (k • p).natDegree = k • p.coeff p.natDegree
⊢ (k • p).leadingCoeff = k • p.leadingCoeff
have rw₃ : k • p.coeff p.natDegree = k • p.coeff p.natDegree
Tactic: rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
    natDegree_smul_of_smul_regular p h]