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
p : R[X]
hp : p.natDegree = 1
n : ℕ
refine_2 :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      0 =
    p.coeff 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      n =
    p.coeff n
have refine_2₁ : (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
    (HAdd.hAdd (α := ℕ) 0 1) =
  p.coeff (HAdd.hAdd (α := ℕ) 0 1)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
refine_2 :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      0 =
    p.coeff 0
refine_2₁ :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      (HAdd.hAdd (α := ℕ) 0 1) =
    p.coeff (HAdd.hAdd (α := ℕ) 0 1)
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      n =
    p.coeff n
have refine_2₂ : ∀ (n : ℕ),
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      (n + 1 + 1) =
    p.coeff (n + 1 + 1)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      (n + 1 + 1) =
    p.coeff (n + 1 + 1)
have refine_2 : 0 = p.coeff (n + 1 + 1)
Tactic: simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ 0 = p.coeff (n + 1 + 1)
have refine_2 : p.natDegree < n + 1 + 1
Tactic: rw [coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : IsLeftCancelMulZero R
h : p.natDegree = 1
r₁ : R
⊢ ∃ (a : R),
    a ≠ 0 ∧
      ∃ (b : R),
        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]) =
          p
have rwa : ∀
  (h :
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          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]) =
            p)
  ⦃r₁ : R⦄,
  ∃ (a : R),
    a ≠ 0 ∧
      ∃ (b : R),
        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]) =
          p
Tactic: rwa [natDegree_eq_one] at h
Cleared hypotheses: h, r₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : IsLeftCancelMulZero R
h : p.natDegree = 1
r₁ : R
⊢ Membership.mem (γ := Set R) {x : R | p.IsRoot x} r₁ →
    ∀ ⦃y : R⦄, Membership.mem (γ := Set R) {x : R | p.IsRoot x} y → r₁ = y
have obtain : ∀ (r₂ : R) (hr₂ : r₂ ≠ 0) (r₃ : R)
  (h :
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r₂ : R[X]) X)
          ((C : (a : R) → R[X]) r₃ : R[X])).natDegree =
      1),
  Membership.mem (γ := Set R)
      {x : R |
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r₂ : R[X]) X)
              ((C : (a : R) → R[X]) r₃ : R[X])).IsRoot
          x}
      r₁ →
    ∀ ⦃y : R⦄,
      Membership.mem (γ := Set R)
          {x : R |
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r₂ : R[X]) X)
                  ((C : (a : R) → R[X]) r₃ : R[X])).IsRoot
              x}
          y →
        r₁ = y
Tactic: obtain ⟨r₂, hr₂, r₃, rfl⟩ : ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p := by rwa [natDegree_eq_one] at h
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsLeftCancelMulZero R
r₁ r₂ : R
hr₂ : r₂ ≠ 0
r₃ : R
h :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r₂ : R[X]) X)
        ((C : (a : R) → R[X]) r₃ : R[X])).natDegree =
    1
⊢ Membership.mem (γ := Set R)
      {x : R |
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r₂ : R[X]) X)
              ((C : (a : R) → R[X]) r₃ : R[X])).IsRoot
          x}
      r₁ →
    ∀ ⦃y : R⦄,
      Membership.mem (γ := Set R)
          {x : R |
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r₂ : R[X]) X)
                  ((C : (a : R) → R[X]) r₃ : R[X])).IsRoot
              x}
          y →
        r₁ = y
have this : ∀ (x y : R) (h : r₂ * x = r₂ * y), x = y
Tactic: have (x y : R) := mul_left_cancel₀ hr₂ (b := x) (c := y)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
a0 : a ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw : p.degree + degree.{u} (R := R) ((C : (a : R) → R[X]) a) = p.degree
Tactic: rw [degree_mul, degree_C a0, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
a0 : a ≠ 0
rw : p.degree + degree.{u} (R := R) ((C : (a : R) → R[X]) a) = p.degree
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw₁ : p.degree + 0 = p.degree
Tactic: rw [degree_mul, degree_C a0, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
a0 : a ≠ 0
rw : p.degree + degree.{u} (R := R) ((C : (a : R) → R[X]) a) = p.degree
rw₁ : p.degree + 0 = p.degree
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw₂ : p.degree = p.degree
Tactic: rw [degree_mul, degree_C a0, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
a0 : a ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have rw : degree.{u} (R := R) ((C : (a : R) → R[X]) a) + p.degree = p.degree
Tactic: rw [degree_mul, degree_C a0, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
a0 : a ≠ 0
rw : degree.{u} (R := R) ((C : (a : R) → R[X]) a) + p.degree = p.degree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have rw₁ : 0 + p.degree = p.degree
Tactic: rw [degree_mul, degree_C a0, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
a0 : a ≠ 0
rw : degree.{u} (R := R) ((C : (a : R) → R[X]) a) + p.degree = p.degree
rw₁ : 0 + p.degree = p.degree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have rw₂ : p.degree = p.degree
Tactic: rw [degree_mul, degree_C a0, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos : ∀ (q0 : q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
Tactic: by_cases q0 : q.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
pos : ∀ (q0 : q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have neg : ∀ (q0 : ¬q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
Tactic: by_cases q0 : q.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos : (p.comp ((C : (a : R) → R[X]) (q.coeff 0))).natDegree =
  p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
Tactic: rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : q.natDegree = 0
pos :
  (p.comp ((C : (a : R) → R[X]) (q.coeff 0))).natDegree =
    p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos₁ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (eval (q.coeff 0) p)) =
  p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
Tactic: rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : q.natDegree = 0
pos :
  (p.comp ((C : (a : R) → R[X]) (q.coeff 0))).natDegree =
    p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
pos₁ :
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (eval (q.coeff 0) p)) =
    p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos₂ : 0 = p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
Tactic: rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : q.natDegree = 0
pos :
  (p.comp ((C : (a : R) → R[X]) (q.coeff 0))).natDegree =
    p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
pos₁ :
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (eval (q.coeff 0) p)) =
    p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
pos₂ : 0 = p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos₃ : 0 = p.natDegree * 0
Tactic: rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : q.natDegree = 0
pos :
  (p.comp ((C : (a : R) → R[X]) (q.coeff 0))).natDegree =
    p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
pos₁ :
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (eval (q.coeff 0) p)) =
    p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
pos₂ : 0 = p.natDegree * natDegree.{u} (R := R) ((C : (a : R) → R[X]) (q.coeff 0))
pos₃ : 0 = p.natDegree * 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos₄ : Eq (α := ℕ) 0 0
Tactic: rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have pos : ∀ (p0 : p = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
Tactic: by_cases p0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : ¬q.natDegree = 0
pos : ∀ (p0 : p = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
have neg : ∀ (p0 : ¬p = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
Tactic: by_cases p0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
have succ : (p.comp (p.comp^[k] q)).natDegree = p.natDegree ^ (k + 1) * q.natDegree
Tactic: rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
succ : (p.comp (p.comp^[k] q)).natDegree = p.natDegree ^ (k + 1) * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
have succ₁ : p.natDegree * (p.comp^[k] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
Tactic: rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
succ : (p.comp (p.comp^[k] q)).natDegree = p.natDegree ^ (k + 1) * q.natDegree
succ₁ : p.natDegree * (p.comp^[k] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
have succ₂ : p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree ^ (k + 1) * q.natDegree
Tactic: rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
succ : (p.comp (p.comp^[k] q)).natDegree = p.natDegree ^ (k + 1) * q.natDegree
succ₁ : p.natDegree * (p.comp^[k] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
succ₂ : p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree ^ (k + 1) * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
have succ₃ : p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree * p.natDegree ^ k * q.natDegree
Tactic: rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
succ : (p.comp (p.comp^[k] q)).natDegree = p.natDegree ^ (k + 1) * q.natDegree
succ₁ : p.natDegree * (p.comp^[k] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
succ₂ : p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree ^ (k + 1) * q.natDegree
succ₃ : p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree * p.natDegree ^ k * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
have succ₄ : p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree * (p.natDegree ^ k * q.natDegree)
Tactic: rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
k : ℕ
⊢ (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
have zero : (p.comp^[0] q).natDegree = HPow.hPow (β := ℕ) p.natDegree 0 * q.natDegree
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
k : ℕ
zero : (p.comp^[0] q).natDegree = HPow.hPow (β := ℕ) p.natDegree 0 * q.natDegree
⊢ (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
have succ : ∀ (k : ℕ) (IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree),
  (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hq : q.natDegree ≠ 0
⊢ (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
have rw : (p.comp q).leadingCoeff = (p.comp q).coeff (p.natDegree * q.natDegree)
Tactic: rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hq : q.natDegree ≠ 0
rw : (p.comp q).leadingCoeff = (p.comp q).coeff (p.natDegree * q.natDegree)
⊢ (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
have rw₁ : (p.comp q).leadingCoeff = (p.comp q).coeff (p.comp q).natDegree
Tactic: rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hq : q.natDegree ≠ 0
rw : (p.comp q).leadingCoeff = (p.comp q).coeff (p.natDegree * q.natDegree)
rw₁ : (p.comp q).leadingCoeff = (p.comp q).coeff (p.comp q).natDegree
⊢ (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
have rw₂ : (p.comp q).leadingCoeff = (p.comp q).leadingCoeff
Tactic: rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).nextCoeff = a * p.nextCoeff
have pos : ∀ (h₀ : a = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).nextCoeff = a * p.nextCoeff
Tactic: by_cases h₀ : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
pos : ∀ (h₀ : a = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).nextCoeff = a * p.nextCoeff
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).nextCoeff = a * p.nextCoeff
have neg : ∀ (h₀ : ¬a = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).nextCoeff = a * p.nextCoeff
Tactic: by_cases h₀ : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).nextCoeff = p.nextCoeff * a
have pos : ∀ (h₀ : a = 0), (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).nextCoeff = p.nextCoeff * a
Tactic: by_cases h₀ : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
pos : ∀ (h₀ : a = 0), (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).nextCoeff = p.nextCoeff * a
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).nextCoeff = p.nextCoeff * a
have neg : ∀ (h₀ : ¬a = 0), (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).nextCoeff = p.nextCoeff * a
Tactic: by_cases h₀ : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
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)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
have pos : ∀ (h : p = 0), (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
pos : ∀ (h : p = 0), (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
have neg : ∀ (h : ¬p = 0), (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : ¬p = 0
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
have neg : p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree =
  HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
Tactic: rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : ¬p = 0
neg :
  p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree =
    HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
have neg₁ : natDegree.{u} (R := R) (-X) ≠ 0
Tactic: rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : ¬p = 0
neg :
  p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree =
    HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
neg₁ : natDegree.{u} (R := R) (-X) ≠ 0
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
have neg₂ : p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree ≠ 0
Tactic: rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree]
-- 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 : eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ p.comp q = 0
have rw : p.comp ((C : (a : R) → R[X]) (q.coeff 0)) = 0
Tactic: 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 : eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
rw : p.comp ((C : (a : R) → R[X]) (q.coeff 0)) = 0
⊢ p.comp q = 0
have rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval (q.coeff 0) p) : R[X]) (0 : R[X])
Tactic: 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 : eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
rw : p.comp ((C : (a : R) → R[X]) (q.coeff 0)) = 0
rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval (q.coeff 0) p) : R[X]) (0 : R[X])
⊢ p.comp q = 0
have rw₂ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
Tactic: 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 : eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
rw : p.comp ((C : (a : R) → R[X]) (q.coeff 0)) = 0
rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval (q.coeff 0) p) : R[X]) (0 : R[X])
rw₂ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
⊢ p.comp q = 0
have rw₃ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [h.2, comp_C, h.1, C_0]