mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal

Tactic:
divisorsAntidiagonalList,

Goal state after:
n : ℕ
⊢ (List.filterMap
        (fun x ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)).toFinset =
    n.divisorsAntidiagonal
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : Fact (1 < n)
h : 0 = 1
⊢ 0 = val 0

Tactic:
val_zero

Goal state after:
m n✝ n : ℕ
inst✝ : Fact (1 < n)
h : 0 = 1
⊢ 0 = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n → n1 * n2 = n ∧ ¬n = 0

Tactic:
intro ⟨⟨hn1, hn2⟩, hn3⟩

Goal state after:
case mpr
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
hn1 : 0 < n1 ∧ n1 ≤ N
hn2 : 0 < n2 ∧ n2 ≤ N
hn3 : n1 * n2 = n
⊢ n1 * n2 = n ∧ ¬n = 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ ↑(n.choose k) < ↑n ^ k / ↑k !

Tactic:
lt_div_iff₀' (mod_cast k.factorial_pos)

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ ↑k ! * ↑(n.choose k) < ↑n ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ n.descFactorial k

Tactic:
rw [choose_eq_descFactorial_div_factorial]
  exact Nat.div_le_self _ _

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val 0 = 0

Tactic:
val_zero

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ 0 = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
⊢ a.val ^ m < n

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
⊢ val 0 ^ m < n

case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(ofDigits b (d :: L)) = ofDigits (↑b) (d :: L)

Tactic:
dsimp [ofDigits]; push_cast; rw [ih]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
by_cases h : n / b = 0

Goal state after:
case pos
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ p * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
Nat.add_sub_add_left

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ p * ofDigits p tl - tl.sum = p * ofDigits p tl - tl.sum
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n → multiplicity a b = n

Tactic:
exact multiplicity_eq_of_emultiplicity_eq_some

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (b.toDigitsCore 0 n []).length ≤ e

Tactic:
simp only [toDigitsCore, List.length, zero_le]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
by classical
  constructor
  · exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)
  · intro h
    unfold emultiplicity
    -- aesop? says
    split
    next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
    next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.natCast_ne_top, imp_false, not_false_eq_true, implies_true]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case succ
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case succ.inl
k : ℕ
ih : (0 ^ k).factorization = k • factorization 0
⊢ (0 ^ (k + 1)).factorization = (k + 1) • factorization 0

case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
f : ℕ →₀ ℕ
hf : f ≤ factorization 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ 0

case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ consFixedLengthDigits hb l i, x.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
simp only [consFixedLengthDigits, cons.injEq, true_and, implies_true, Set.injOn_of_eq_iff_eq,
        Finset.sum_image, sum_cons]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ fixedLengthDigits hb l, (i + x.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ (n.factorization + (f - n.factorization)).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
Finsupp.prod_add_index' (by simp) Nat.pow_add,

Goal state after:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n.factorization.prod HPow.hPow * (f - n.factorization).prod HPow.hPow
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ (1 ^ n) ^ 0 = 1

Tactic:
one_pow,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ 1 ^ 0 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

Tactic:
unfold orderOf

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 ↦ x * x_1) 1 / (minimalPeriod (fun x_1 ↦ x * x_1) 1).gcd n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

Tactic:
unfold orderOf

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 ↦ x * x_1) 1 / (minimalPeriod (fun x_1 ↦ x * x_1) 1).gcd n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) 1 ∣ (orderOf x).lcm (orderOf y)

Tactic:
exact Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n

Tactic:
have h1 : n / d ≠ 0 := by simp [*]

Goal state after:
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
rw [pow_dvd_pow_iff_le_right pp.one_lt]

Goal state after:
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ a.factorization p ≤ b.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n ≡ m [MOD orderOf x]
⊢ n = m

Tactic:
orderOf_eq_zero_iff.mpr h,

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n ≡ m [MOD 0]
⊢ n = m
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n d : ℕ
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0

case inr
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n ≡ m [MOD orderOf x]
⊢ n = m

Tactic:
orderOf_eq_zero_iff.mpr h,

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n ≡ m [MOD 0]
⊢ n = m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ x ^ (orderOf x - 1) * x = 1

Tactic:
rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
    exact (isOfFinOrder_of_finite x).orderOf_pos

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LeftCancelMonoid G
inst✝² : Finite G
x y : G
n : ℕ
H : Type u_6
inst✝¹ : RightCancelMonoid H
inst✝ : Finite H
⊢ Group H

Tactic:
letI : Finite Hᵐᵒᵖ := Finite.of_equiv H MulOpposite.opEquiv
  letI : Group Hᵐᵒᵖ := LeftCancelMonoid.groupOfFinite (G := Hᵐᵒᵖ)
  exact (MulEquiv.opOp H).toEquiv.group

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
p : ℕ
pp : Prime p
⊢ Icc 1 ((factorization 0) p) = {i ∈ Ico 1 0 | p ^ i ∣ 0}

case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x

Tactic:
coe_iterateFrobenius,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (⇑(frobenius R p))^[m * n] x = (⇑(frobenius R p))^[m]^[n] x
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ∃ d, g' = g + d
⊢ ¬¬∃ g₂, g' = g + g₂

Tactic:
rwa [Classical.not_not]

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) + (expand R p) ((expand R q) g) = (expand R (p * q)) f + (expand R (p * q)) g

Tactic:
ihf,

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 * 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 + (expand R 1) g = f + g

Tactic:
ihf,

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
⊢ f + (expand R 1) g = f + g
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
· rw [hf, map_zero, natDegree_zero, zero_mul]

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).Monic ↔ f.Monic

Tactic:
simp only [Monic, leadingCoeff_expand hp]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p, x.2 * p).1 * ((expand R p) g).coeff (x.1 * p, x.2 * p).2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

Tactic:
simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
derivative_of_natDegree_zero hp,

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ (⇑derivative)^[t] 0 = 0
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
⊢ ¬p.degree < q.degree

Tactic:
not_lt

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial.succ.zero
R : Type u
inst✝ : Semiring R
a b : R
m : ℕ
⊢ (monomial (m + 1 + 0 - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + 0 - 1)) (a * (b * ↑0)) =
    (monomial (m + 1 - 1 + 0)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (0 - 1))) (a * (b * ↑0))

Tactic:
simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
have h₄ : degree (r - f %ₘ g) < degree g :=
    calc
      degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) := degree_sub_le _ _
      _ < degree g := max_lt_iff.2 ⟨h.2, degree_modByMonic_lt _ hg⟩

Goal state after:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
⊢ f /ₘ g = q ∧ f %ₘ g = r
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] p = k ! • ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x

Tactic:
by
  conv_lhs => rw [iterate_derivative_eq_sum]
  rw [smul_sum]
  refine sum_congr rfl fun i _ ↦ ?_
  rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
⊢ ¬(n + 1) • p.coeff (n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0

Tactic:
smul_eq_zero

Goal state after:
R : Type u
n : ℕ
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
⊢ ¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : (X - C a) * (p /ₘ (X - C a)) = p
⊢ eval a p = 0

Tactic:
← h,

Goal state after:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : (X - C a) * (p /ₘ (X - C a)) = p
⊢ eval a ((X - C a) * (p /ₘ (X - C a))) = 0
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i ↦ s i (ind i)

Tactic:
by
  rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩
  choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
  exact ⟨ind, hp, hd.mono ht⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : ∀ (n : ℕ), (derivative p).coeff n = coeff 0 n
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : (m + 1) • p.coeff (m + 1) = 0
⊢ False

Tactic:
smul_eq_zero

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : ∀ (n : ℕ), (derivative p).coeff n = coeff 0 n
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : m + 1 = 0 ∨ p.coeff (m + 1) = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁

Tactic:
sub_eq_iff_eq_add.mp sub_eq,

Goal state after:
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ 0 = (comp 0 (X + C t)).trailingCoeff

Tactic:
zero_comp,

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ 0 = trailingCoeff 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)
⊢ (⇑derivative)^[k + 1] ((X + C c) ^ n) = n.descFactorial (k + 1) • (X + C c) ^ (n - (k + 1))

Tactic:
| succ k IH =>

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

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

Tactic:
simp_rw [iterate_derivative_mul, iterate_derivative_X_pow_eq_smul, mul_smul]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
⊢ p = q

Tactic:
by
  rcases eq_or_ne q 0 with rfl | hq
  · simpa using h₂
  replace h₁ := (natDegree_le_of_dvd hpq hq).antisymm h₁
  obtain ⟨u, rfl⟩ := hpq
  rw [mul_ne_zero_iff] at hq
  rw [natDegree_mul hq.1 hq.2, left_eq_add] at h₁
  rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂
  rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
⊢ (⇑derivative)^[k + 1] P = 0

Tactic:
rw [Function.iterate_add_apply, Function.iterate_one]

Goal state after:
R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : s ∈ f.support
⊢ f s • w s ≤ f s • w s + ∑ x ∈ f.support \ {s}, f x • w x

Tactic:
exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)

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

Goal state before:
pp: case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a (if h : p = 0 then ∅ else Classical.choose ⋯) = rootMultiplicity a p

Tactic:
dif_neg hp

Goal state after:
case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a (Classical.choose ⋯) = rootMultiplicity a p