mathlib-initiative/mathlib-tactics huggingface dataset:
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
ha : a ≠ 0
⊢ a.val > 0

Tactic:
rwa [gt_iff_lt, ZMod.val_pos]

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

Goal state before:
pp: case succ
b k : ℕ
ih : ofDigits b (List.replicate k 0) = 0
⊢ ofDigits b (List.replicate (k + 1) 0) = 0

Tactic:
| succ k ih =>

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

Goal state before:
pp: m k n : ℕ
⊢ (n ∈ Set.range fun n ↦ m * n + k) ↔ n ∈ {n | ↑n = ↑k ∧ k ≤ n}

Tactic:
simp only [Set.mem_range, Set.mem_ofPred_eq]

Goal state after:
m k n : ℕ
⊢ (∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0
⊢ d :: L ≠ []

Tactic:
by simp

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

Goal state before:
pp: p n : ℕ
⊢ n = p ^ padicValNat p n * n.divMaxPow p

Tactic:
by simp

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

Goal state before:
pp: b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ x ∈ l, x < b
⊢ ofDigits b l < b ^ l.length

Tactic:
by
  rcases b with (_ | _ | b) <;> simp_all [ofDigits_lt_base_pow_length']

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

Goal state before:
pp: case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
| succ k ih =>

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

Goal state before:
pp: case inr.inr
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : p < 1
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
· simp [lt_one_iff.mp h]
    cases L
    · rfl
    · simp [ofDigits]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
b : α
⊢ ¬FiniteMultiplicity 1 b

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ multiplicity a b = multiplicity a b

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p n : ℕ
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn₀; · simp
  rcases eq_or_ne p 1 with rfl | hp₁; · simp
  simpa [*] using pow_dvd_iff_le_padicValNat (k := 1) hp₁ hn₀ |>.symm |>.not

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:
| succ k ih =>

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ ∀ (a : ℕ), a ^ 0 = 1

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Prime p
b : ℕ
x✝ : log p 0 < b
⊢ 0!.factorization p = ∑ i ∈ Ico 1 b, 0 / p ^ i

Tactic:
by simp

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

Goal state before:
pp: p n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ∣ n ↔ p ^ 1 ∣ n

Tactic:
by simp

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ ((n + k).choose k).factorization p + (k ! * n !).factorization p =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (k ! * n !).factorization p

Tactic:
have h2 := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ((n + k).choose k).factorization p + (k ! * n !).factorization p =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (k ! * n !).factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p x : ℕ
x✝¹ : x + 1 ≤ 0
x✝ : x + 1 ≠ 0
⊢ (factorization 0) p ≤ (choose 0 (x + 1)).factorization p + (x + 1).factorization p

Tactic:
by simp

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

Goal state before:
pp: case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i < b

Tactic:
zero_pow,

Goal state after:
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ∣ n
⊢ i < b

case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i ≠ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card (Fin (orderOf a)) = orderOf a

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) =
    ↑(∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0))

Tactic:
sum_add_distrib,

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) =
    ↑(∑ x ∈ Ico 1 b, n / p ^ x + ∑ x ∈ Ico 1 b, if p ^ x ∣ n + 1 then 1 else 0)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
⊢ x ^ m = 1 * x ^ m

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ m = 1 * a ^ m

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card (Fin (orderOf a)) = orderOf a

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

pp: case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
· rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
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✝ : Group G
x y : G
i : ℤ
hx : IsOfFinOrder x
n : ℕ
⊢ (fun x_1 ↦ x ^ x_1) ↑n = x ^ n

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]
  nth_rw 2 [← one_pow (p ^ n)]
  rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]

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

Goal state before:
pp: β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
obtain rfl | hm₀ := eq_or_ne m 0

Goal state after:
case inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
⊢ (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f

case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
x✝ : ℕ
⊢ emultiplicity p x✝ ≤ emultiplicity p (x✝.choose 0) + emultiplicity p 0

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Prime p
n✝ : ℕ
⊢ emultiplicity p 0 ≤ emultiplicity p (choose 0 (n✝ + 1)) + emultiplicity p (n✝ + 1)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (n : ℕ), (p + q).divX.coeff n = (p.divX + q.divX).coeff n

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |(-1)| = 1
⊢ (-1) ^ 2 = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
⊢ (expand R (p ^ Nat.zero)) f = (⇑(expand R p))^[Nat.zero] f

Tactic:
by rw [pow_zero, expand_one, Function.iterate_zero, id]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)

Tactic:
rw [derivative_apply]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)).coeff n = p.coeff (n + 1) * (↑n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r a : R
⊢ eval r ((expand R p) (C a)) = eval (r ^ p) (C a)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
n : ℕ
a : R
x✝ : eval r ((expand R p) (C a * X ^ n)) = eval (r ^ p) (C a * X ^ n)
⊢ eval r ((expand R p) (C a * X ^ (n + 1))) = eval (r ^ p) (C a * X ^ (n + 1))

Tactic:
by simp

Goal state after:
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
a : R
⊢ (aeval r) ((expand R p) (C a)) = (aeval (r ^ p)) (C a)

Tactic:
by simp

Goal state after:
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
n : ℕ
a : R
x✝ : (aeval r) ((expand R p) (C a * X ^ n)) = (aeval (r ^ p)) (C a * X ^ n)
⊢ (aeval r) ((expand R p) (C a * X ^ (n + 1))) = (aeval (r ^ p)) (C a * X ^ (n + 1))

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a) = 0

Tactic:
by simp [derivative_apply]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (monomial (1 - 1)) (1 * ↑1) = 1

Tactic:
by simp

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

Goal state before:
pp: case succ
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p
p : R[X]
⊢ (⇑derivative)^[k + 1] (s • p) = s • (⇑derivative)^[k + 1] p

Tactic:
| succ k ih =>

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ x.1 * p + x.2 * p = (x.1 + x.2) * p

Tactic:
add_mul

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ((⇑derivative)^[0] p).natDegree ≤ p.natDegree - 0

Tactic:
rw [Function.iterate_zero_apply, Nat.sub_zero]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
⊢ (expand R p) (contract p f) = f

Tactic:
ext n
  rw [coeff_expand hp.bot_lt, coeff_contract hp]
  split_ifs with h
  · rw [Nat.div_mul_cancel h]
  · rcases n with - | n
    · exact absurd (dvd_zero p) h
    have := coeff_derivative f n
    rw [hf, coeff_zero, zero_eq_mul] at this
    rcases this with h' | _
    · rw [h']
    rename_i _ _ _ h'
    rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'
    exact absurd h' h

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ (x ::ₘ t).card = Add.add (↑t.card) 1

Tactic:
exact mod_cast Multiset.card_cons _ _

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

Goal state before:
pp: case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)
p : R[X]
⊢ (⇑derivative)^[k + 1] (map f p) = map f ((⇑derivative)^[k + 1] p)

Tactic:
| succ k ih =>

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))

Tactic:
expand_expand

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R (p * p ^ n)) f)
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (⇑(aeval x) ∘ fun x ↦ X - C x) x = 0

Tactic:
by simp

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

Goal state before:
pp: case succ
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 : ℕ
⊢ ((⇑derivative)^[k + 1] p).coeff m = (m + (k + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))

Tactic:
| succ k ih =>

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
a✝ : Nontrivial R
⊢ ∀ (i : ℕ), (monomial i) 0 = 0

Tactic:
by simp

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:
← pow_succ',

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 ^ (i - (n + 1 + 1) + 1) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
p✝ : R[X]
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ map f 0 = 0

Tactic:
by simp

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)

Tactic:
rw [derivative_apply]

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)).degree ≤ ↑(p.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
i : ℕ
⊢ s ↑(x i) ∈ f

Tactic:
by cases i <;> apply hs.set_index_mem

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

Goal state before:
pp: α : Type u_1
a : α
⊢ (pure a).IsCountablyGenerated

Tactic:
rw [← principal_singleton]
  exact isCountablyGenerated_principal _

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ 𝓟 ⊤ ≤ f ↔ f = ⊤

Tactic:
by simp

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)^[k + 1] (X ^ n) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))

Tactic:
| succ k ih =>

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
⊢ s i ∈ f i

Tactic:
rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi

Goal state after:
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))
⊢ ∀ a ∈ range n.succ,
    a ∈ range (min m n).succ →
      (n.choose a * m.descFactorial a) • ((⇑derivative)^[n - a] p * X ^ (m - a)) =
        (n.choose a * m.descFactorial a) • ((⇑derivative)^[n - a] p * X ^ (m - a))

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
t : Set ((i : ι) → α i)
⊢ (∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, True) ∧ (i.1.pi fun i ↦ s i) ⊆ t) ↔ ∃ I, I.Finite ∧ I.pi s ⊆ t

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Tactic:
by_cases hi : i ∈ I

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
hi : i ∈ I
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

case neg
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
hi : i ∉ I
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
f : Filter α
hf : f.sets.Finite
B : Set α
⊢ ∀ U ∈ f.sets, U ∈ f

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Finite α
f : Filter α
⊢ f.sets ⊆ 𝒫 univ

Tactic:
by simp

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

Goal state before:
pp: case succ.zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0 + 1 + 2] p * X ^ 2 + (2 * (0 + 1)) • (⇑derivative)^[0 + 1 + 1] p * X +
      ((0 + 1) * (0 + 1 - 1)) • (⇑derivative)^[0 + 1] p =
    ∑ k ∈ range (min 2 (0 + 1)).succ,
      ((0 + 1).choose k * Nat.descFactorial 2 k) • ((⇑derivative)^[0 + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

Tactic:
simp [sum_range_succ, ← mul_assoc]

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

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

Tactic:
add_mul

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
⊢ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i ∈ map (f i) (l i)

Tactic:
by_cases hi : i ∈ I

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∈ I
⊢ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i ∈ map (f i) (l i)

case neg
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∉ I
⊢ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i ∈ map (f i) (l i)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
inst✝ : Finite ι
f : (i : ι) → α i → β i
l : (i : ι) → Filter (α i)
⊢ ∀ᶠ (i : ι) in cofinite, Surjective (f i)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
⊢ pure a ×ˢ pure b = pure (a, b)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s : Multiset ι
f : ι → R[X]
⊢ derivative (Multiset.map f 0).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (Multiset.erase 0 i)).prod * derivative (f i)) 0).sum

Tactic:
by simp

Goal state after: