mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ M f

Tactic:
suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
  refine Polynomial.induction_on f ?_ ?_ ?_
  · exact fun a => Or.inl (natDegree_C _)
  · rintro p q (hp | hp) (hq | hq)
    · refine Or.inl ?_
      rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hp]
      exact h_C_add hq
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hq, add_comm]
      exact h_C_add hp
    · exact Or.inr (h_add hp hq)
  · intro n a _
    by_cases a0 : a = 0
    · exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
    · refine Or.inr ?_
      rw [C_mul_X_pow_eq_monomial]
      exact h_monomial a0 n.succ_ne_zero

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f✝ f g : R[X]
ihf : (expand R p) ((expand R q) f) = (expand R (p * q)) f
ihg : (expand R p) ((expand R q) g) = (expand R (p * q)) g
⊢ (expand R p) ((expand R q) (f + g)) = (expand R (p * q)) (f + g)

Tactic:
map_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f✝ f g : R[X]
ihf : (expand R p) ((expand R q) f) = (expand R (p * q)) f
ihg : (expand R p) ((expand R q) g) = (expand R (p * q)) g
⊢ (expand R p) ((expand R q) f) + (expand R p) ((expand R q) g) = (expand R (p * q)) f + (expand R (p * q)) g
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ (expand R 1) (f + g) = f + g

Tactic:
map_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ (expand R 1) f + (expand R 1) g = f + g
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) (f + g)) = eval (r ^ p) (f + g)

Tactic:
map_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) f + (expand R p) g) = eval (r ^ p) (f + g)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree →
    (if h : q.Monic then
          (if q.degree ≤ p.degree ∧ ¬p = 0 then
              (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
            else (0, p)).2
        else p).degree <
      q.degree

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree →
    (if q.degree ≤ p.degree ∧ ¬p = 0 then
            (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
          else (0, p)).2.degree <
      q.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ (if h : q.Monic then
        (if q.degree ≤ p.degree ∧ ¬p = 0 then
            (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
          else (0, p)).2
      else p).degree <
    q.degree

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).2.degree <
    q.degree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval r) ((expand R p) (f + g)) = (aeval (r ^ p)) (f + g)

Tactic:
map_add,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval r) ((expand R p) f + (expand R p) g) = (aeval (r ^ p)) (f + g)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).2
    else p) =
    p

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if q.degree ≤ p.degree ∧ ¬p = 0 then
        (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
          ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
      else (0, p)).2 =
    p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
        have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
        have _wf := ⋯;
        have dm := (p - q * z).divModByMonicAux ⋯;
        (z + dm.1, dm.2)
      else (0, p)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q *
        if hq : q.Monic then ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1
        else 0) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1 =
    p -
      q *
        (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux ⋯;
            (z + dm.1, dm.2)
          else (0, p)).1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if q.degree ≤ p.degree ∧ ¬p = 0 then
              (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
            else (0, p)).1
        else 0

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (if q.degree ≤ p.degree ∧ ¬p = 0 then
        (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
          ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
      else (0, p)).2 =
    p -
      q *
        if h : q.Monic then
          (if q.degree ≤ p.degree ∧ ¬p = 0 then
              (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
            else (0, p)).1
        else 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).2 =
    p -
      q *
        if h : q.Monic then
          (if q.degree ≤ p.degree ∧ ¬p = 0 then
              (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
            else (0, p)).1
        else 0

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).2 =
    p -
      q *
        (if q.degree ≤ p.degree ∧ ¬p = 0 then
            (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
          else (0, p)).1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).1
    else 0) =
    0

Tactic:
dif_pos hq,

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if q.degree ≤ p.degree ∧ ¬p = 0 then
        (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
          ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
      else (0, p)).1 =
    0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) (a + b)) = (a + b) ^ p

Tactic:
map_add,

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) a + (expand R p) b) = (a + b) ^ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
    calc
      degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
      _ ≤ _ := by
        rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
            Nat.cast_add, Nat.cast_le]
        exact Nat.le_add_right _ _

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ q.degree + (p /ₘ q).degree = p.degree
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ (¬∃ p, p ≠ 0 ∧ (aeval x) p = 0) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
not_exists

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ (aeval x) x_1 = 0)) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q * p %ₘ q = 0

Tactic:
by
  rw [modByMonic_eq_zero_iff_dvd hq]
  exact dvd_mul_right q p

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
← mul_assoc,

Goal state after:
case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a * a ^ (i - (n + 1 + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * ((X - C a) * q) = p
⊢ False

Tactic:
← mul_assoc,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * (X - C a) * q = p
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n * p ^ n * p + C 1 * p ^ n * p) * derivative p + p ^ n * p * derivative p =
    C (↑n.succ + 1) * (p ^ n * p) * derivative p

Tactic:
← mul_assoc,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n * p ^ n * p + C 1 * p ^ n * p) * derivative p + p ^ n * p * derivative p =
    C (↑n.succ + 1) * p ^ n * p * derivative p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
⊢ (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))

Tactic:
rw [hsum]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
⊢ ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) =
    ∑ k ∈ range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
⊢ derivative (p.comp q) = derivative q * (derivative p).comp q

Tactic:
induction p using Polynomial.induction_on'

Goal state after:
case add
R : Type u
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : derivative (p✝.comp q) = derivative q * (derivative p✝).comp q
a✝ : derivative (q✝.comp q) = derivative q * (derivative q✝).comp q
⊢ derivative ((p✝ + q✝).comp q) = derivative q * (derivative (p✝ + q✝)).comp q

case monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * (X ^ n * X))) = eval₂ C q (derivative (C r * (X ^ n * X))) * derivative q

Tactic:
← mul_assoc,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * X ^ n * X)) = eval₂ C q (derivative (C r * X ^ n * X)) * derivative q
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ f ≤ ￢f

Tactic:
le_cofinite_iff_ker,

Goal state after:
α : Type u_2
f : Filter α
⊢ f.ker = ∅ ↔ f ≤ ￢f