mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * a.val = n

Tactic:
rw [neg_eq_iff_add_eq_zero, ← two_mul]

Goal state after:
n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * val 0

Tactic:
rw [val_zero, mul_zero]

Goal state after:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
⊢ b.digitsAux h n = n % b :: b.digitsAux h (n / b)

Tactic:
cases n
  · cases w
  · rw [digitsAux]

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

Goal state before:
pp: m k n : ℕ
| (∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n

Tactic:
conv =>

Goal state after:
m k n y : ℕ
| n = k + m * y
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append✝ : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
h_append : b.digits n ≠ []
⊢ (b.digits n).getLast ⋯ ≠ 0

Tactic:
exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append

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

Goal state before:
pp: case cons
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
l2 : List ℕ
h : (hd₁ :: tl₁).length = l2.length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) l2)

Tactic:
| cons hd₁ tl₁ ih₁ =>

Goal state after:
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 - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) + ∑ i ∈ Ico 1 (tl.length + 1), ofDigits p (List.drop i tl) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
← sum_Ico_add _ 0 tl.length 1,

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 - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) + ∑ x ∈ Ico 0 tl.length, ofDigits p (List.drop (1 + x) tl) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
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 - 1) * ∑ k ∈ range 1, ofDigits p (List.drop k tl) +
        (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) +
      (p - 1) * ofDigits p [] =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
ih,

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 - 1) * ∑ k ∈ range 1, ofDigits p (List.drop k tl) + (ofDigits p tl - tl.sum) + (p - 1) * ofDigits p [] =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p (List.drop 1 (List.drop i digits)) = ofDigits p (List.drop (i + 1) digits)

Tactic:
List.drop_drop,

Goal state after:
case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p (List.drop (i + 1) digits) = ofDigits p (List.drop (i + 1) digits)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case bit
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b ↦ bif b then 1 else 0) (b :: n.bits)

Tactic:
cases b

Goal state after:
case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

case bit.true
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit true n) = List.map (fun b ↦ bif b then 1 else 0) (true :: n.bits)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
by
  by_cases hf : FiniteMultiplicity a b
  · simp [hf.emultiplicity_eq_multiplicity]
  · simp [hf, emultiplicity_eq_top.2]

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 : β
h : emultiplicity a b = emultiplicity c d
⊢ multiplicity a b = multiplicity c d

Tactic:
unfold multiplicity

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ WithTop.untopD 1 (emultiplicity a b) = WithTop.untopD 1 (emultiplicity c d)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length

Tactic:
induction f with (simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>
    if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial

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

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
conv =>

Goal state after:
case b
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits 1 (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
conv =>

Goal state after:
case b
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ofDigits c (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l x✝ : ℕ
h : x✝ ∈ {n | n < b ^ l}
⊢ (b.digitsAppend l x✝).length = l

Tactic:
rw [length_digitsAppend hb _ h]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ (↑(Finset.range b)).PairwiseDisjoint fun d ↦ consFixedLengthDigits hb l d

Tactic:
refine Finset.pairwiseDisjoint_iff.mpr fun i _ j _ ⟨L, hL⟩ ↦ ?_
  rw [Finset.mem_inter] at hL
  exact (consFixedLengthDigits_head hb hL.1).symm.trans (consFixedLengthDigits_head hb hL.2)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
h : x ^ n = 1
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1

Tactic:
rwa [isPeriodicPt_mul_iff_pow_eq_one]

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

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

Tactic:
ih,

Goal state after:
case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ n.factorization + k • n.factorization = (k + 1) • n.factorization
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2

Tactic:
induction l with
  | zero => simp
  | succ l hr =>
      by_cases hl : l = 0
      · simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]
      rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]
      simp only [consFixedLengthDigits, cons.injEq, true_and, implies_true, Set.injOn_of_eq_iff_eq,
        Finset.sum_image, sum_cons]
      rw [Finset.sum_comm]
      simp_rw [Finset.sum_add_distrib, Finset.sum_const, Finset.sum_nsmul, Finset.sum_range_id, hr,
        nsmul_eq_mul, Finset.card_range, add_tsub_cancel_right, cast_id, card_fixedLengthDigits,
        choose_two_right]
      rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]
      ring

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2

Tactic:
← List.sum_fixedLengthDigits_sum hb

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = ∑ L ∈ List.fixedLengthDigits hb l, L.sum
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hk
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ ¬IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ n) 1

Tactic:
rwa [isPeriodicPt_mul_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hk1
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ (n + 1)) 1

Tactic:
rwa [isPeriodicPt_mul_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
by
  wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  rw [pow_add, (hx.isUnit.pow _).mul_eq_left, pow_eq_one_iff_modEq]
  exact ⟨fun h ↦ Nat.ModEq.add_left _ h, fun h ↦ Nat.ModEq.add_left_cancel' _ h⟩

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.lcm b).factorization = a.factorization ⊔ b.factorization

Tactic:
by
  rw [← add_right_inj (a.gcd b).factorization, ←
    factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
    factorization_gcd ha hb, factorization_mul ha hb]
  ext1
  exact (min_add_max _ _).symm

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ ↑(orderOf x) ∣ -(m - n) ↔ ↑(orderOf x) ∣ n - m

Tactic:
neg_sub

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ ↑(orderOf x) ∣ n - m ↔ ↑(orderOf x) ∣ n - m
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ Nat.Prime (ringChar R)

Tactic:
apply CharP.char_prime_of_ne_zero R
  exact CharP.ringChar_ne_zero_of_finite R

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
cases b

Goal state after:
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ emultiplicity 2 (bit false n)! < ↑(bit false n)

case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = orderOf x * card (G ⧸ zpowers x)

Tactic:
rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
⊢ p.divX.degree < p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ p.divX.degree < p.degree
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝¹ : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst✝ : Finite ι
this : Fintype ι
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x

Tactic:
simp only [← orderOf_ne_zero_iff, Pi.orderOf]

Goal state after:
ι : Type u_6
α : ι → Type u_7
inst✝¹ : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst✝ : Finite ι
this : Fintype ι
⊢ (∀ (i : ι), orderOf (x i) ≠ 0) → (Finset.univ.lcm fun i ↦ orderOf (x i)) ≠ 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
intro hn
      rw [notMem_support_iff.1 hn]
      split_ifs <;> rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ ↑q.natDegree ≤ ↑p.natDegree

Tactic:
rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]; exact h.1

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

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n b : ℕ
⊢ b ∈ p.support → b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

Tactic:
cases b

Goal state after:
case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ 0 ∈ p.support → 0 ≠ n + 1 → (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ n✝ + 1 ∈ p.support → n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 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
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (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
inst✝ : Algebra.IsAlgebraic R A
p : R[X]
hp : p ≠ 0
⊢ Nontrivial R

Tactic:
exact .of_polynomial_ne hp

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

Goal state before:
pp: case inr.refine_1
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
⊢ p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
ih,

Goal state after:
case inr.refine_1
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
⊢ p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ rootMultiplicity a (C r) = 0

Tactic:
classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]

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
this : ¬p.coeff (n + 1) * ↑(n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0
⊢ n ∈ (derivative p).support ↔ n + 1 ∈ p.support

Tactic:
by
    simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]

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

Goal state before:
pp: case bot
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ ⊥ < 1 → ⊥ ≤ 0

Tactic:
exact fun _ => bot_le

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

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

Tactic:
nontriviality R
  have h : (p %ₘ (X - C a)).eval a = p.eval a := by
    rw [modByMonic_eq_sub_mul_div, eval_sub, eval_mul, eval_sub, eval_X,
      eval_C, sub_self, zero_mul, sub_zero]
  have : degree (p %ₘ (X - C a)) < 1 :=
    degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
  have : degree (p %ₘ (X - C a)) ≤ 0 := by
    revert this
    cases degree (p %ₘ (X - C a))
    · exact fun _ => bot_le
    · exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))
  rw [eq_C_of_degree_le_zero this, eval_C] at h
  rw [eq_C_of_degree_le_zero this, h]

Goal state after:
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) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < (X - C a).degree

Tactic:
rw [degree_X_sub_C]; decide

Goal state after:
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
iInf_eq_generate,

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ generate (⋃ i, (s i).sets) → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
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
⊢ derivative (p ^ (n + 1)) * p + p ^ (n + 1) * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p

Tactic:
ih,

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 + 1) * p ^ n * derivative p * p + p ^ (n + 1) * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - 1) ∣ derivative p

Tactic:
obtain ⟨r, rfl⟩ := dvd
  rw [derivative_mul, derivative_pow]
  exact (((dvd_mul_left _ _).mul_right _).mul_right _).add ((pow_dvd_pow q n.pred_le).mul_right _)

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

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

Tactic:
ih,

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ derivative (↑(n.descFactorial k) * X ^ (n - k)) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case insert
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
⊢ ⨅ i_1 ∈ insert i s, 𝓟 (f i_1) = 𝓟 (⋂ i_1 ∈ insert i s, f i_1)

Tactic:
Finset.iInf_insert,

Goal state after:
case insert
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
⊢ 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (⋂ i_1 ∈ insert i s, f i_1)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Tactic:
simpa only [Filter.Eventually, ofPred_forall] using biInter_mem hI

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff * u.coeff 0 = p.leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u

Tactic:
mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
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)) * q + eval₂ C q (C r * X ^ n) * derivative q =
    eval₂ C q (derivative (C r * X ^ n * X)) * derivative q

Tactic:
ih,

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
⊢ eval₂ C q (derivative (C r * X ^ n)) * derivative q * q + eval₂ C q (C r * X ^ n) * derivative q =
    eval₂ C q (derivative (C r * X ^ n * X)) * derivative q