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
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X n) + p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₂ : (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
⊢ p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HPow.hPow (α := R[X]) X n + p.eraseLead
have refine_1₃ : 1 * HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
Tactic: rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X n) + p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₂ : (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₃ : 1 * HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
⊢ p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HPow.hPow (α := R[X]) X n + p.eraseLead
have refine_1₄ : HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
Tactic: rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.eraseLead.natDegree < n
have refine_2 : p.natDegree - 1 < n
Tactic: refine p.eraseLead_natDegree_le.trans_lt ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.natDegree - 1 < n
have refine_2 : n - 1 < n
Tactic: rw [hp.natDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
⊢ (p * q).IsMonicOfDegree (m + n)
have inl : ∀ (H : Subsingleton R), (p * q).IsMonicOfDegree (m + 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 : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
inl : ∀ (H : Subsingleton R), (p * q).IsMonicOfDegree (m + n)
⊢ (p * q).IsMonicOfDegree (m + n)
have inr : ∀ (H : Nontrivial R), (p * q).IsMonicOfDegree (m + 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 : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Subsingleton R
⊢ (p * q).IsMonicOfDegree (m + n)
have inl : ∀ (hp : m = 0) (hq : n = 0), m = 0 ∧ n = 0
Tactic: simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hp hq ⊢
Cleared hypotheses: hp, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).IsMonicOfDegree (m + n)
have inr : (p * q).natDegree = m + n
Tactic: refine ⟨?_, hp.monic.mul hq.monic⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have rw : Ne.{u_1 + 1} (α := R) 1 0
Tactic: rw [hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).natDegree = m + n
have this : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_mul]
    exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).natDegree = m + n
have inr : p.natDegree + q.natDegree = m + n
Tactic: rw [natDegree_mul' this, hp.natDegree_eq, hq.natDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
this : p.leadingCoeff * q.leadingCoeff ≠ 0
inr : p.natDegree + q.natDegree = m + n
⊢ (p * q).natDegree = m + n
have inr₁ : m + q.natDegree = m + n
Tactic: rw [natDegree_mul' this, hp.natDegree_eq, hq.natDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
this : p.leadingCoeff * q.leadingCoeff ≠ 0
inr : p.natDegree + q.natDegree = m + n
inr₁ : m + q.natDegree = m + n
⊢ (p * q).natDegree = m + n
have inr₂ : m + n = m + n
Tactic: rw [natDegree_mul' this, hp.natDegree_eq, hq.natDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
⊢ (p ^ n).IsMonicOfDegree (m * n)
have zero : (HPow.hPow (β := ℕ) p 0).IsMonicOfDegree (m * 0)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, mul_add, mul_one]
    exact ih.mul hp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).IsMonicOfDegree (m * 0)
⊢ (p ^ n).IsMonicOfDegree (m * n)
have succ : ∀ (n : ℕ) (ih : (p ^ n).IsMonicOfDegree (m * n)), (p ^ (n + 1)).IsMonicOfDegree (m * (n + 1))
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, mul_add, mul_one]
    exact ih.mul hp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
m : ℕ
hm : n ≤ m
⊢ p.coeff m = q.coeff m
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
m : ℕ
hm : n ≤ m
h : Nontrivial R
⊢ p.coeff m = q.coeff m
have rw : ∀ (hp : p.natDegree ≤ n ∧ p.coeff n = 1) (hq : q.natDegree ≤ n ∧ q.coeff n = 1) {m : ℕ} (hm : n ≤ m),
  Nontrivial R → p.coeff m = q.coeff m
Tactic: rw [isMonicOfDegree_iff] at hp hq
Cleared hypotheses: hp, hq, m, hm, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm : n ≤ m
h : Nontrivial R
⊢ p.coeff m = q.coeff m
have inl : ∀ (hm : n ≤ n), p.coeff n = q.coeff n
Tactic: rcases eq_or_lt_of_le hm with rfl | hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm : n ≤ m
h : Nontrivial R
inl : ∀ (hm : n ≤ n), p.coeff n = q.coeff n
⊢ p.coeff m = q.coeff m
have inr : ∀ (hm : n < m), p.coeff m = q.coeff m
Tactic: rcases eq_or_lt_of_le hm with rfl | hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
h : Nontrivial R
hm : n ≤ n
⊢ p.coeff n = q.coeff n
have inl : 1 = q.coeff n
Tactic: rw [hp.2, hq.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
h : Nontrivial R
hm : n ≤ n
inl : 1 = q.coeff n
⊢ p.coeff n = q.coeff n
have inl₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [hp.2, hq.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm_1 : n ≤ m
h : Nontrivial R
hm : n < m
⊢ p.coeff m = q.coeff m
have hp₁ : p.natDegree < m
Tactic: replace hp : p.natDegree < m := hp.1.trans_lt hm
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm_1 : n ≤ m
h : Nontrivial R
hm : n < m
hp : p.natDegree < m
⊢ p.coeff m = q.coeff m
have hq₁ : q.natDegree < m
Tactic: replace hq : q.natDegree < m := hq.1.trans_lt hm
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n m : ℕ
hm_1 : n ≤ m
h : Nontrivial R
hm : n < m
hp : p.natDegree < m
hq : q.natDegree < m
⊢ p.coeff m = q.coeff m
have inr : 0 = q.coeff m
Tactic: rw [coeff_eq_zero_of_natDegree_lt hp, coeff_eq_zero_of_natDegree_lt hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n m : ℕ
hm_1 : n ≤ m
h : Nontrivial R
hm : n < m
hp : p.natDegree < m
hq : q.natDegree < m
inr : 0 = q.coeff m
⊢ p.coeff m = q.coeff m
have inr₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt hp, coeff_eq_zero_of_natDegree_lt hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
⊢ q.IsMonicOfDegree n
have inl : ∀ (H : Subsingleton R), q.IsMonicOfDegree 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 : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
inl : ∀ (H : Subsingleton R), q.IsMonicOfDegree n
⊢ q.IsMonicOfDegree n
have inr : ∀ (H : Nontrivial R), q.IsMonicOfDegree 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 : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
⊢ q.IsMonicOfDegree n
have inl : ∀ (hpq : m = 0 ∧ n = 0), n = 0
Tactic: simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hpq ⊢
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
⊢ q.IsMonicOfDegree n
have h₂ : q.Monic
Tactic: have h₂ : q.Monic := hp.monic.of_mul_monic_left hpq.monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
⊢ q.IsMonicOfDegree n
have inr : q.natDegree = n
Tactic: refine ⟨?_, h₂⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
⊢ q.natDegree = n
have this : (p * q).natDegree = m + n
Tactic: have := hpq.natDegree_eq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have rw : Ne.{u_1 + 1} (α := R) 1 0
Tactic: rw [hp.leadingCoeff_eq, h₂.leadingCoeff, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ q.natDegree = n
have h : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: have h : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, h₂.leadingCoeff, one_mul]
    exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n
have this₁ : m + q.natDegree = m + n
Tactic: rw [natDegree_mul' h, hp.natDegree_eq] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
⊢ p.IsMonicOfDegree m
have inl : ∀ (H : Subsingleton R), p.IsMonicOfDegree m
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 : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
inl : ∀ (H : Subsingleton R), p.IsMonicOfDegree m
⊢ p.IsMonicOfDegree m
have inr : ∀ (H : Nontrivial R), p.IsMonicOfDegree m
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 : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
⊢ p.IsMonicOfDegree m
have inl : ∀ (hpq : m = 0 ∧ n = 0), m = 0
Tactic: simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hpq ⊢
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
⊢ p.IsMonicOfDegree m
have h₂ : p.Monic
Tactic: have h₂ : p.Monic := hq.monic.of_mul_monic_right hpq.monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
⊢ p.IsMonicOfDegree m
have inr : p.natDegree = m
Tactic: refine ⟨?_, h₂⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
⊢ p.natDegree = m
have this : (p * q).natDegree = m + n
Tactic: have := hpq.natDegree_eq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have rw : Ne.{u_1 + 1} (α := R) 1 0
Tactic: rw [h₂.leadingCoeff, hq.leadingCoeff_eq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
⊢ p.natDegree = m
have h : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: have h : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [h₂.leadingCoeff, hq.leadingCoeff_eq, one_mul]
    exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.natDegree = m
have this₁ : p.natDegree + n = m + n
Tactic: rw [natDegree_mul' h, hq.natDegree_eq] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p + q).IsMonicOfDegree n
have inl : ∀ (H : Subsingleton R), (p + q).IsMonicOfDegree 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 : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
inl : ∀ (H : Subsingleton R), (p + q).IsMonicOfDegree n
⊢ (p + q).IsMonicOfDegree n
have inr : ∀ (H : Nontrivial R), (p + q).IsMonicOfDegree 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 : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Nontrivial R
⊢ (p + q).IsMonicOfDegree n
have inr : (p + q).natDegree ≤ n
Tactic: refine (isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Nontrivial R
inr : (p + q).natDegree ≤ n
⊢ (p + q).IsMonicOfDegree n
have inr₁ : (p + q).coeff n = 1
Tactic: refine (isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Nontrivial R
⊢ (p + q).coeff n = 1
have inr : p.coeff n = 1
Tactic: rw [coeff_add_eq_left_of_lt hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree < n
hq : q.IsMonicOfDegree n
⊢ (p + q).IsMonicOfDegree n
have rw : (q + p).IsMonicOfDegree n
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
⊢ (p.comp q).IsMonicOfDegree (m * n)
have inl : ∀ (h : Subsingleton R), (p.comp q).IsMonicOfDegree (m * 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 : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
inl : ∀ (h : Subsingleton R), (p.comp q).IsMonicOfDegree (m * n)
⊢ (p.comp q).IsMonicOfDegree (m * n)
have inr : ∀ (h : Nontrivial R), (p.comp q).IsMonicOfDegree (m * 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 : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Subsingleton R
⊢ (p.comp q).IsMonicOfDegree (m * n)
have inl : ∀ (hp : m = 0), m = 0 ∨ n = 0
Tactic: simp only [isMonicOfDegree_iff_of_subsingleton, mul_eq_zero] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (m * n)
have inr : (p.comp q).IsMonicOfDegree (p.natDegree * q.natDegree)
Tactic: rw [← hp.natDegree_eq, ← hq.natDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (p.natDegree * q.natDegree)
have inr : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
Tactic: refine (isMonicOfDegree_iff ..).mpr ⟨natDegree_comp_le, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1
have inr : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
Tactic: rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
inr : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1
have inr₁ : 1 * q.leadingCoeff ^ p.natDegree = 1
Tactic: rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
inr : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
inr₁ : 1 * q.leadingCoeff ^ p.natDegree = 1
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1
have inr₂ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
Tactic: rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
inr : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
inr₁ : 1 * q.leadingCoeff ^ p.natDegree = 1
inr₂ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1
have inr₃ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
inr : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
inr₁ : 1 * q.leadingCoeff ^ p.natDegree = 1
inr₂ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
inr₃ : HMul.hMul (α := R) 1 1 = 1
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1
have inr₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring 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]