awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
⊢ (map f p).natDegree = p.natDegree

Tactic:
natDegree_eq_of_degree_eq <| degree_map_eq_of_injective hf _

Premises used: Polynomial.degree_map_eq_of_injective, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
⊢ (map f p).leadingCoeff = (f : (a : R) → S) p.leadingCoeff

Tactic:
simp only [leadingCoeff, natDegree_map_eq_of_injective hf, coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.leadingCoeff, Polynomial.natDegree_map_eq_of_injective
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
simp :
  (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    (f : (a : R) → S) (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))
⊢ (map f p).nextCoeff = (f : (a : R) → S) p.nextCoeff

Tactic:
simp only [hf, nextCoeff, natDegree_map_eq_of_injective]

Premises used: Polynomial.nextCoeff, Polynomial.natDegree_map_eq_of_injective
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
pos : p.natDegree = 0 → Eq.{v + 1} (α := S) (0 : S) ((f : (a : R) → S) 0 : S)
neg : ¬p.natDegree = 0 → (map f p).coeff (p.natDegree - 1) = (f : (a : R) → S) (p.coeff (p.natDegree - 1))
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    (f : (a : R) → S) (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
h : p.natDegree = 0
⊢ Eq.{v + 1} (α := S) (0 : S) ((f : (a : R) → S) 0 : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
h : ¬p.natDegree = 0
⊢ (map f p).coeff (p.natDegree - 1) = (f : (a : R) → S) (p.coeff (p.natDegree - 1))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.nextCoeff ≠ 0
⊢ 0 < p.natDegree

Tactic:
grind [nextCoeff]

Premises used: Polynomial.nextCoeff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p q : R[X]
rw : (-(p - q)).natDegree = (q - p).natDegree
rw₁ rw₂ : (q - p).natDegree = (q - p).natDegree
⊢ (p - q).natDegree = (q - p).natDegree

Tactic:
rw [← natDegree_neg, neg_sub]

Premises used: neg_sub, Polynomial.natDegree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
qn : q.natDegree ≤ n
⊢ (-q).natDegree ≤ n

Tactic:
rw [← natDegree_neg] at qn

Premises used: Polynomial.natDegree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
rw : (p + -q).natDegree ≤ n ↔ p.natDegree ≤ n
rw₁ rw₂ : p.natDegree ≤ n ↔ p.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]

Premises used: sub_eq_add_neg, Polynomial.natDegree_add_le_iff_left
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
pn : p.natDegree ≤ n
rwa : (q - p).natDegree ≤ n ↔ q.natDegree ≤ n
rwa₁ : q.natDegree ≤ n ↔ q.natDegree ≤ n
rwa₂ : p.natDegree ≤ n
rwa₃ : q.natDegree ≤ n ↔ q.natDegree ≤ n
rwa₄ rwa₅ rwa₆ : p.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
rwa [natDegree_sub, natDegree_sub_le_iff_left]

Premises used: Polynomial.natDegree_sub_le_iff_left, Polynomial.natDegree_sub
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
dg : q.natDegree < n
⊢ (-q).natDegree < n

Tactic:
rw [← natDegree_neg] at dg

Premises used: Polynomial.natDegree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
dg : (-q).natDegree < n
rw : (p + -q).coeff n = p.coeff n
rw₁ rw₂ : p.coeff n = p.coeff n
⊢ (p - q).coeff n = p.coeff n

Tactic:
rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]

Premises used: Polynomial.coeff_add_eq_left_of_lt, sub_eq_add_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
df : p.natDegree < n
rwa : (p + -q).coeff n = -q.coeff n
rwa₁ : (-q).coeff n = -q.coeff n
rwa₂ : p.natDegree < n
rwa₃ : -q.coeff n = -q.coeff n
rwa₄ : p.natDegree < n
rwa₅ : -q.coeff n = -q.coeff n
rwa₆ rwa₇ rwa₈ : p.natDegree < n
⊢ (p - q).coeff n = -q.coeff n

Tactic:
rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]

Premises used: sub_eq_add_neg, Polynomial.coeff_add_eq_right_of_lt, Polynomial.coeff_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
a : R
ha : a ≠ 0
c : R
rw :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).coeff
      ((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) c : R[X])).natDegree -
        1) =
    c
rw₁ :
  0 <
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).natDegree
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).nextCoeff =
    c

Tactic:
rw [nextCoeff_of_natDegree_pos]

Premises used: Polynomial.nextCoeff_of_natDegree_pos
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
a : R
ha : a ≠ 0
c : 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]) c : R[X])).coeff
      ((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) c : R[X])).natDegree -
        1) =
    c

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ 0 <
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).natDegree

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.natDegree = 1 ↔
    ∃ (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:
⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩

Premises used: Polynomial.coeff, And.intro, Iff.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
refine_1 : ∀ (hp : p.natDegree = 1) (h : p.coeff 1 = 0), False
refine_2 :
  ∀ (hp : p.natDegree = 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]) =
      p
refine_3 :
  (∃ (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) →
    p.natDegree = 1
⊢ p.natDegree = 1 ↔
    ∃ (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:
refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff 1 = 0
⊢ p = 0

Tactic:
rw [← hp, coeff_natDegree, leadingCoeff_eq_zero] at h

Premises used: Polynomial.coeff_natDegree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
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 =
      p.coeff 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]) =
    p

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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)
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)
⊢ (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

Tactic:
obtain _ | _ | n := n
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 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
      0 =
    p.coeff 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 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
      (HAdd.hAdd (α := ℕ) 0 1) =
    p.coeff (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
refine_2 : 0 = p.coeff (n + 1 + 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 + 1 + 1) =
    p.coeff (n + 1 + 1)

Tactic:
simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]

Premises used: Polynomial.coeff_mul_X, Polynomial.coeff_add, Polynomial.coeff_C_succ, add_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
refine_2 : p.natDegree < n + 1 + 1
⊢ 0 = p.coeff (n + 1 + 1)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ p.natDegree < n + 1 + 1

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
a : R
ha : 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])).natDegree =
    1

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : IsLeftCancelMulZero R
h : p.natDegree = 1
r₁ : R
rwa rwa₁ rwa₂ 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
⊢ ∃ (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

Premises used: Polynomial.natDegree_eq_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : IsLeftCancelMulZero R
h : p.natDegree = 1
r₁ : R
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
⊢ Membership.mem (γ := Set R) {x : R | p.IsRoot x} r₁ →
    ∀ ⦃y : R⦄, Membership.mem (γ := Set R) {x : R | p.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

Premises used: Polynomial.X, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
⊢ ∀ (x y : R) (h : r₂ * x = r₂ * y), x = y

Tactic:
have (x y : R) := mul_left_cancel₀ hr₂ (b := x) (c := y)
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
this : ∀ (x y : R) (h : r₂ * x = r₂ * y), x = y
⊢ 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:
grind [IsRoot, eval_add, eval_mul_X, eval_C]

Premises used: Polynomial.eval_C, Polynomial.IsRoot, Polynomial.eval_add, Polynomial.eval_mul_X
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
rw₂ rw₃ : p.degree = p.degree
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree

Tactic:
rw [degree_mul, degree_C a0, add_zero]

Premises used: Polynomial.degree_C, add_zero, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
rw₂ rw₃ : p.degree = p.degree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree

Tactic:
rw [degree_mul, degree_C a0, zero_add]

Premises used: Polynomial.degree_C, zero_add, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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])).natDegree = p.natDegree

Tactic:
simp only [natDegree, degree_mul_C a0]

Premises used: Polynomial.natDegree, Polynomial.degree_mul_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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).natDegree = p.natDegree

Tactic:
simp only [natDegree, degree_C_mul a0]

Premises used: Polynomial.degree_C_mul, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
neg : ∀ (q0 : ¬q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases q0 : q.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
pos₄ pos₅ : Eq (α := ℕ) 0 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]

Premises used: Polynomial.comp_C, Polynomial.natDegree_C, MulZeroClass.mul_zero, Iff.mp, Polynomial.degree_le_zero_iff, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
neg : ∀ (p0 : ¬p = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases p0 : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
simp only [p0, zero_comp, natDegree_zero, zero_mul]

Premises used: Polynomial.zero_comp, MulZeroClass.zero_mul, Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
        ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]

Premises used: pow_ne_zero, Polynomial.natDegree_comp_eq_of_mul_ne_zero, Ne, mul_eq_zero, Polynomial.ne_zero_of_natDegree_gt, Nat.pos_of_ne_zero, or_self, not_false_eq_true, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
⊢ (p.comp^[0] q).natDegree = HPow.hPow (β := ℕ) p.natDegree 0 * q.natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
succ₄ 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

Tactic:
rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]

Premises used: Function.iterate_succ_apply', Polynomial.natDegree_comp, mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
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
⊢ (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree

Tactic:
induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]

Premises used: Function.iterate_succ_apply', Polynomial.natDegree_comp, mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
rw₂ rw₃ : (p.comp q).leadingCoeff = (p.comp q).leadingCoeff
⊢ (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]

Premises used: Polynomial.coeff_natDegree, Polynomial.natDegree_comp, Polynomial.coeff_comp_degree_mul_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
neg : ∀ (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

Tactic:
by_cases h₀ : a = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
h₀ : a = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).nextCoeff = a * p.nextCoeff

Tactic:
simp [h₀, nextCoeff, natDegree_C_mul]

Premises used: Polynomial.natDegree_C_mul, Polynomial.nextCoeff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
h₀ : ¬a = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).nextCoeff = a * p.nextCoeff

Tactic:
simp [h₀, nextCoeff, natDegree_C_mul]

Premises used: Polynomial.natDegree_C_mul, Polynomial.nextCoeff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
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
neg : ∀ (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

Tactic:
by_cases h₀ : a = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
h₀ : a = 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).nextCoeff = p.nextCoeff * a

Tactic:
simp [h₀, nextCoeff, natDegree_mul_C]

Premises used: Polynomial.nextCoeff, Polynomial.natDegree_mul_C