awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
⊢ p.comp q = 0 ↔ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
have refine : ∀ (h : p.comp q = 0), p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
Tactic: refine ⟨fun h ↦ ?_, Or.rec (fun h ↦ by simp [h]) fun h ↦ by rw [h.2, comp_C, h.1, C_0]⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0
have rw : p.natDegree * q.natDegree = 0
Tactic: rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
rw : p.natDegree * q.natDegree = 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0
have rw₁ : (p.comp q).natDegree = 0
Tactic: rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
rw : p.natDegree * q.natDegree = 0
rw₁ : (p.comp q).natDegree = 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0
have rw₂ : natDegree.{u} (R := R) 0 = 0
Tactic: rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
rw : p.natDegree * q.natDegree = 0
rw₁ : (p.comp q).natDegree = 0
rw₂ : natDegree.{u} (R := R) 0 = 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0
have rw₃ : Eq (α := ℕ) 0 0
Tactic: rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
have key : p.natDegree = 0 ∨ q.natDegree = 0
Tactic: have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
    rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key : p.natDegree = 0 ∨ q.natDegree = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
have inl : ∀ (key : p = (C : (a : R) → R[X]) (p.coeff 0)), p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
Tactic: obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key : p.natDegree = 0 ∨ q.natDegree = 0
inl :
  ∀ (key : p = (C : (a : R) → R[X]) (p.coeff 0)), p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
have inr : ∀ (key : q = (C : (a : R) → R[X]) (q.coeff 0)), p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
Tactic: obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
have h₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
Tactic: rw [key, C_comp] at h
Cleared hypotheses: h, key_1, key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
have h₁ : eval (q.coeff 0) p = 0
Tactic: rw [key, comp_C, C_eq_zero] at h
Cleared hypotheses: h, key_1, key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
⊢ (p.comp q).degree = p.degree * q.degree
have inl : (comp 0 q).degree = degree.{u} (R := R) 0 * q.degree
Tactic: rcases eq_or_ne p 0 with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
inl : (comp 0 q).degree = degree.{u} (R := R) 0 * q.degree
⊢ (p.comp q).degree = p.degree * q.degree
have inr : ∀ (hp : p ≠ 0), (p.comp q).degree = p.degree * q.degree
Tactic: rcases eq_or_ne p 0 with rfl | hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ (comp 0 q).degree = degree.{u} (R := R) 0 * q.degree
have inl : Eq (α := WithBot ℕ) ⊥ (if q.degree = 0 then 0 else ⊥)
Tactic: rw [zero_comp, degree_zero, WithBot.bot_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = p.degree * q.degree
have inr : (p.comp q).degree = (↑(p.comp q).natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree hp, degree_eq_natDegree (ne_zero_of_degree_gt hq), ← Nat.cast_mul,
    ← natDegree_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = (↑(p.comp q).natDegree : WithBot ℕ)
have inr : p.comp q ≠ 0
Tactic: apply degree_eq_natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ p.comp q ≠ 0
have inr : ¬eval (q.coeff 0) p = 0 ∨ ¬q.degree ≤ 0
Tactic: simp_rw [Ne, comp_eq_zero_iff, hp, false_or, not_and_or, ← degree_le_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (p.comp (-X)).degree = p.degree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
⊢ (p.comp (-X)).degree = p.degree
have inl : degree.{u} (R := R) (comp 0 (-X)) = degree.{u} (R := R) 0
Tactic: rcases eq_or_ne p 0 with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
inl : degree.{u} (R := R) (comp 0 (-X)) = degree.{u} (R := R) 0
⊢ (p.comp (-X)).degree = p.degree
have inr : ∀ (hp : p ≠ 0), (p.comp (-X)).degree = p.degree
Tactic: rcases eq_or_ne p 0 with rfl | hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
⊢ degree.{u} (R := R) (comp 0 (-X)) = degree.{u} (R := R) 0
have inl : degree.{u} (R := R) 0 = degree.{u} (R := R) 0
Tactic: rw [zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
⊢ (p.comp (-X)).degree = p.degree
have inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
Tactic: rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
⊢ (p.comp (-X)).degree = p.degree
have inr₁ : Eq (α := WithBot ℕ) (↑(p.comp (-X)).natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
inr₁ : Eq (α := WithBot ℕ) (↑(p.comp (-X)).natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
⊢ (p.comp (-X)).degree = p.degree
have inr₂ : (p.comp (-X)).natDegree = p.natDegree
Tactic: rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
inr₁ : Eq (α := WithBot ℕ) (↑(p.comp (-X)).natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
inr₂ : (p.comp (-X)).natDegree = p.natDegree
⊢ (p.comp (-X)).degree = p.degree
have inr₃ : p.natDegree * natDegree.{u} (R := R) (-X) = p.natDegree
Tactic: rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
inr₁ : Eq (α := WithBot ℕ) (↑(p.comp (-X)).natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
inr₂ : (p.comp (-X)).natDegree = p.natDegree
inr₃ : p.natDegree * natDegree.{u} (R := R) (-X) = p.natDegree
⊢ (p.comp (-X)).degree = p.degree
have inr₄ : p.natDegree * natDegree.{u} (R := R) X = p.natDegree
Tactic: rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
inr₁ : Eq (α := WithBot ℕ) (↑(p.comp (-X)).natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
inr₂ : (p.comp (-X)).natDegree = p.natDegree
inr₃ : p.natDegree * natDegree.{u} (R := R) (-X) = p.natDegree
inr₄ : p.natDegree * natDegree.{u} (R := R) X = p.natDegree
⊢ (p.comp (-X)).degree = p.degree
have inr₅ : p.natDegree * 1 = p.natDegree
Tactic: rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
inr₁ : Eq (α := WithBot ℕ) (↑(p.comp (-X)).natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
inr₂ : (p.comp (-X)).natDegree = p.natDegree
inr₃ : p.natDegree * natDegree.{u} (R := R) (-X) = p.natDegree
inr₄ : p.natDegree * natDegree.{u} (R := R) X = p.natDegree
inr₅ : p.natDegree * 1 = p.natDegree
⊢ (p.comp (-X)).degree = p.degree
have inr₆ : p.natDegree = p.natDegree
Tactic: rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
⊢ Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p
have pos : ∀ (hp0 : p = 0), Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
pos :
  ∀ (hp0 : p = 0), Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p
⊢ Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p
have neg : ∀ (hp0 : ¬p = 0), Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).Monic
have rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).leadingCoeff = 1
Tactic: rw [Monic, leadingCoeff_mul, leadingCoeff_C,
    mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
h : p ≠ 0
rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).leadingCoeff = 1
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).Monic
have rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = 1
Tactic: rw [Monic, leadingCoeff_mul, leadingCoeff_C,
    mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
h : p ≠ 0
rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).leadingCoeff = 1
rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = 1
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).Monic
have rw₂ : p.leadingCoeff * p.leadingCoeff⁻¹ = 1
Tactic: rw [Monic, leadingCoeff_mul, leadingCoeff_C,
    mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
h : p ≠ 0
rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).leadingCoeff = 1
rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = 1
rw₂ : p.leadingCoeff * p.leadingCoeff⁻¹ = 1
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).Monic
have rw₃ : Eq.{u_1 + 1} (α := K) 1 1
Tactic: rw [Monic, leadingCoeff_mul, leadingCoeff_C,
    mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
p q : K[X]
h : q ≠ 0
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) q.leadingCoeff⁻¹ : K[X])).degree = p.degree
have h₁ : q.leadingCoeff⁻¹ ≠ 0
Tactic: have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p q : K[X]
h : q ≠ 0
h₁ : q.leadingCoeff⁻¹ ≠ 0
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) q.leadingCoeff⁻¹ : K[X])).degree = p.degree
have rw : p.degree = p.degree
Tactic: rw [degree_mul_C h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
have pos : ∀ (hp : p = 0), (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
pos : ∀ (hp : p = 0), (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
have neg : ∀ (hp : ¬p = 0), (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
⊢ p.degree + degree.{u_1} (R := K) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = p.degree
have rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
Tactic: rw [← degree_mul, degree_mul_leadingCoeff_self_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
⊢ p.degree + degree.{u_1} (R := K) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = p.degree
have rw₁ : p.degree = p.degree
Tactic: rw [← degree_mul, degree_mul_leadingCoeff_self_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hf : p.natDegree ≤ n
hn : p.coeff n = 0
⊢ p.natDegree ≤ n - 1
have zero : ∀ (hf : p.natDegree ≤ 0) (hn : p.coeff 0 = 0), p.natDegree ≤ HSub.hSub (α := ℕ) 0 1
Tactic: obtain _ | n := n
Cleared hypotheses: n, hf, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hf : p.natDegree ≤ n
hn : p.coeff n = 0
zero : ∀ (hf : p.natDegree ≤ 0) (hn : p.coeff 0 = 0), p.natDegree ≤ HSub.hSub (α := ℕ) 0 1
⊢ p.natDegree ≤ n - 1
have succ : ∀ (n : ℕ) (hf : p.natDegree ≤ n + 1) (hn : p.coeff (n + 1) = 0), p.natDegree ≤ n + 1 - 1
Tactic: obtain _ | n := n
Cleared hypotheses: n, hf, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1
have succ : ∀ (h : p.natDegree = n.succ), False
Tactic: refine (Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
h : p.natDegree = n.succ
⊢ False
have hn₁ : p = 0
Tactic: rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn
Cleared hypotheses: hn, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ (monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff = p
have rcases : ∀ (n : ℕ) (a : R) (h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1),
  Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1
⊢ Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
have pos : ∀ (ha : a = 0),
  Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1
pos :
  ∀ (ha : a = 0),
    Eq (α := R[X])
      ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
          (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
        R[X])
      ((monomial n : (a : R) → R[X]) a : R[X])
⊢ Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
have neg : ∀ (ha : ¬a = 0),
  Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ (monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff = p
have rcases : ∀ (n : ℕ) (a : R) (h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1),
  Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: classical
  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
  by_cases ha : a = 0 <;> simp [ha]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) = p
have rw : (monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff = p
Tactic: rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : #p.support ≤ 1
rw : (monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff = p
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) = p
have rw₁ : p = p
Tactic: rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : Subsingleton R
⊢ p.degree = ⊥
have rw : degree.{u} (R := R) 0 = ⊥
Tactic: rw [Subsingleton.elim p 0, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : Subsingleton R
rw : degree.{u} (R := R) 0 = ⊥
⊢ p.degree = ⊥
have rw₁ : Eq (α := WithBot ℕ) ⊥ ⊥
Tactic: rw [Subsingleton.elim p 0, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : Subsingleton R
⊢ p.natDegree = 0
have rw : natDegree.{u} (R := R) 0 = 0
Tactic: rw [Subsingleton.elim p 0, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : Subsingleton R
rw : natDegree.{u} (R := R) 0 = 0
⊢ p.natDegree = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [Subsingleton.elim p 0, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ n ≤ p.natDegree
have rw : (↑n : WithBot ℕ) ≤ p.degree
Tactic: rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
rw : (↑n : WithBot ℕ) ≤ p.degree
⊢ n ≤ p.natDegree
have rw₁ : p ≠ 0
Tactic: rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
⊢ p.natDegree < q.natDegree
have pos : ∀ (hq : q = 0), p.natDegree < q.natDegree
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
pos : ∀ (hq : q = 0), p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree
have neg : ∀ (hq : ¬q = 0), p.natDegree < q.natDegree
Tactic: by_cases hq : q = 0