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

Goal state before:
pp: case refine_3
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)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
intro n

Goal state after:
case refine_3
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)
n : ℕ
⊢ ∀ (a : R), (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
⊢ False

Tactic:
have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ False
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 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

Tactic:
if_neg h,

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
⊢ (0, p).2.degree < q.degree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 1
hg : g.degree = 0
⊢ IsUnit f

pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ IsUnit f

Tactic:
· simp [← not_lt, hf, hg] at H

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ (f.coeff (x, y).1 * if p ∣ (x, y).2 then g.coeff ((x, y).2 / p) else 0) = 0

Tactic:
if_neg h,

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ f.coeff (x, y).1 * 0 = 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)
⊢ (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

Tactic:
if_neg h,

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 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 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

Tactic:
if_neg h,

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 * (0, p).1
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hp : 0 ≠ 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
exact hp rfl

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p

Tactic:
frobenius_def

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C (a ^ p) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.add
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
p✝ q✝ : R[X]
a✝¹ : derivative ((monomial m) a * p✝) = derivative ((monomial m) a) * p✝ + (monomial m) a * derivative p✝
a✝ : derivative ((monomial m) a * q✝) = derivative ((monomial m) a) * q✝ + (monomial m) a * derivative q✝
⊢ derivative ((monomial m) a * (p✝ + q✝)) =
    derivative ((monomial m) a) * (p✝ + q✝) + (monomial m) a * derivative (p✝ + q✝)

Tactic:
simp only [mul_add, map_add, add_assoc, add_left_comm, *]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
intro n

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree

pp: case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree

Tactic:
· exact (le_of_eq (by simp only [h0, natDegree_zero])).trans_lt hq

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)

Tactic:
by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q +
          -(C q.leadingCoeff * (p * X ^ (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree)))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0

Tactic:
simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ ∀ b ∈ p.support, ((fun n a ↦ C (a * ↑n) * X ^ (n - 1)) b (p.coeff b)).degree ≤ ↑(p.natDegree - 1)

Tactic:
intro n

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
n : ℕ
⊢ n ∈ p.support → ((fun n a ↦ C (a * ↑n) * X ^ (n - 1)) n (p.coeff n)).degree ≤ ↑(p.natDegree - 1)
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ↑I) → ι' ↑i
hsub : ⋂ i, s (↑i) (⟨I, f⟩.snd i) ⊆ t
hI : ⟨I, f⟩.fst.Finite
hf : ∀ (i : ↑⟨I, f⟩.fst), p (↑i) (⟨I, f⟩.snd i)
⊢ ⋂ i, s (↑i) (⟨I, f⟩.snd i) ∈ ⨅ i, l i

Tactic:
cases hI.nonempty_fintype

Goal state after:
case refine_2.intro
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ↑I) → ι' ↑i
hsub : ⋂ i, s (↑i) (⟨I, f⟩.snd i) ⊆ t
hI : ⟨I, f⟩.fst.Finite
hf : ∀ (i : ↑⟨I, f⟩.fst), p (↑i) (⟨I, f⟩.snd i)
val✝ : Fintype ↑⟨I, f⟩.fst
⊢ ⋂ i, s (↑i) (⟨I, f⟩.snd i) ∈ ⨅ i, l i
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
⊢ (⨅ i, f i).IsCountablyGenerated

Tactic:
choose s hs using fun i => exists_antitone_basis (f i)
  rw [← PLift.down_surjective.iInf_comp]
  refine HasCountableBasis.isCountablyGenerated ⟨.iInf fun n => (hs _).1, ?_⟩
  refine (countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_
  rintro ⟨I, f⟩ ⟨hI, -⟩
  lift I to Finset (PLift ι) using hI
  exact ⟨⟨I, f⟩, rfl⟩

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

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

Tactic:
by rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative ↑n = 0

Tactic:
by
  rw [← C_eq_intCast n]
  exact derivative_C

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ (⇑derivative)^[n] ((X - C c) ^ n) = ↑n !

Tactic:
rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ (k ::ₘ c ::ₘ s).prod ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
refine multiset_prod_mem _ _ (Multiset.forall_mem_cons.2 ⟨subset_closure ?_,
          Multiset.forall_mem_cons.2 ⟨subset_closure ?_, fun t ht => subset_closure (hs t ht)⟩⟩)

Goal state after:
case cons.inl.refine_1.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ k ∈ {r | IsUnit r ∨ Prime r}

case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c ∈ {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
⊢ Multiset.map (fun x ↦ a * x + b) (p.comp (C a * X + C b)).roots = p.roots

Tactic:
by
  classical
  set f := fun x ↦ a * x + b
  have hf : Function.Bijective f :=
    (AddGroup.addRight_bijective b).comp (IsUnit.isUnit_iff_mulLeft_bijective.mp ha)
  rw [Multiset.ext]
  intro x
  obtain ⟨x, rfl⟩ := hf.surjective x
  rw [count_roots, count_map_eq_count' f _ hf.injective, count_roots,
    rootMultiplicity_comp_C_mul_X_add_C p a b x ha]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ hd.roots + tl.prod.roots = (hd ::ₘ ↑tl).bind roots

Tactic:
Multiset.cons_bind,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ hd.roots + tl.prod.roots = hd.roots + (↑tl).bind roots
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
⊢ p.IsPrimitive

Tactic:
rintro r ⟨q, hq⟩

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
⊢ IsUnit r
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * if p = 0 then 1 else Classical.choose ⋯

Tactic:
if_neg h,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * Classical.choose ⋯
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a : R
⊢ ∀ (p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
p

Goal state after:
case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
⊢ a ≠ 0 →
    Prime p →
      (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
        p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
by_cases h : p = 0
  · simp only [h, map_zero, rootMultiplicity_zero]
  obtain ⟨g, hp, hndvd⟩ := p.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h t
  set m := p.rootMultiplicity t
  have hm : m - 1 + 1 = m := Nat.sub_add_cancel <| (rootMultiplicity_pos h).2 hpt
  have hndvd : ¬(X - C t) ^ m ∣ derivative p := by
    rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _),
      derivative_X_sub_C_pow, ← hm, pow_succ, hm, mul_comm (C _), mul_assoc,
      dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]
    rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢
    rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
  have hnezero : derivative p ≠ 0 := fun h ↦ hndvd (by rw [h]; exact dvd_zero _)
  exact le_antisymm (by rwa [rootMultiplicity_le_iff hnezero, hm])
    (rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero _ t hnezero)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s (C p.content) * eval₂ f s p.primPart = 0
⊢ eval₂ f s p.primPart = 0

Tactic:
eval₂_C

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : f p.content * eval₂ f s p.primPart = 0
⊢ eval₂ f s p.primPart = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
⊢ ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
n : ℕ
⊢ ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
n : ℕ
⊢ ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)

Tactic:
p

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q : R[X]
a✝ : Nontrivial R
n : ℕ
p : R[X]
⊢ ∀ (q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ ∃ q, (Multiset.map (fun a ↦ X - C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
obtain ⟨q, he⟩ := p.prod_multiset_X_sub_C_dvd

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
⊢ ∃ q, (Multiset.map (fun a ↦ X - C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
p : FactorSet α
⊢ p.prod = 0 ↔ p = ⊤

Tactic:
by
  unfold FactorSet at p
  induction p  -- TODO: `induction_eliminator` doesn't work with `abbrev`
  · simp only [Associates.prod_top]
  · rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
      iff_false, not_exists]
    exact fun a => not_and_of_not_right _ a.prop.ne_zero

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = C (p.coeff 0) * C (p.coeff 0)⁻¹

Tactic:
rw [← C_mul, mul_inv_cancel₀ hc, C_1]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
⊢ q.degree + (p / q).degree = p.degree

Tactic:
by
  have : degree (p % q) < degree (q * (p / q)) :=
    calc
      degree (p % q) < degree q := EuclideanDomain.mod_lt _ hq0
      _ ≤ _ := degree_le_mul_left _ (mt (Polynomial.div_eq_zero_iff hq0).1 (not_lt_of_ge hpq))
  conv_rhs =>
    rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]

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

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (C q.leadingCoeff⁻¹) * map f (p /ₘ (q * C q.leadingCoeff⁻¹)) =
    C (map f q).leadingCoeff⁻¹ * (map f p /ₘ (map f q * C (map f q).leadingCoeff⁻¹))

Tactic:
map_divByMonic f (monic_mul_leadingCoeff_inv hq0),

Goal state after:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (C q.leadingCoeff⁻¹) * (map f p /ₘ map f (q * C q.leadingCoeff⁻¹)) =
    C (map f q).leadingCoeff⁻¹ * (map f p /ₘ (map f q * C (map f q).leadingCoeff⁻¹))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
⊢ p ∣ a

Tactic:
rcases eq_or_ne a 0 with rfl | ha0
  · exact dvd_zero p
  obtain ⟨a0, nza, ha'⟩ := exists_non_zero_rep ha0
  rw [← Associates.factors_prod a]
  rw [← ha', factors_mk a0 nza] at hm ⊢
  rw [prod_coe]
  apply Multiset.dvd_prod; apply Multiset.mem_map.mpr
  exact ⟨⟨p, irreducible_of_mem_factorSet hm⟩, mem_factorSet_some.mp hm, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq : q ≠ 0
⊢ (p % q).degree < q.degree

Tactic:
rw [Polynomial.mod_def]

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq : q ≠ 0
⊢ (p %ₘ (q * C q.leadingCoeff⁻¹)).degree < q.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
⊢ (p₁ + p₂) % q = p₁ % q + p₂ % q

Tactic:
simp [Polynomial.mod_def, Polynomial.add_modByMonic]

Goal state after: