mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ i (nj j) ∈ M'

Tactic:
· rw [← hc, piEquiv_apply_apply]
        refine Submodule.sum_mem _ fun j' _ ↦ ?_
        let c' : A := ⟨c j j', Subring.subset_closure
          (by simp [show ∃ a b, c a b = c j j' from ⟨j, j', rfl⟩])⟩
        rw [show c j j' • mj j' = c' • mj j' from rfl]
        exact smul_mem _ _ (subset_span (by simp))

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
⊢ let leq := ⋯;
  (quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯) = (quotientMap I f' ⋯).comp (quotientMap (comap f' I) g leq)

Tactic:
refine RingHom.ext fun a => ?_

Goal state after:
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
a : R ⧸ comap f (comap g' I)
⊢ ((quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯)) a =
    ((quotientMap I f' ⋯).comp (quotientMap (comap f' I) g ⋯)) a
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_2.mp
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) → l.Nodup

pp: case refine_2.mpr
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ l.Nodup → ∃ a, a.val = ↑l

Tactic:
· intro h
      rcases h with ⟨f, hf⟩
      convert! f.nodup
      rw [hf]
      rfl

Goal state after:
case refine_2.mpr
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ l.Nodup → ∃ a, a.val = ↑l
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
⊢ [].permutations = [[]]

Tactic:
rw [permutations, permutationsAux_nil]

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ (permutations'Aux x as).Disjoint (permutations'Aux x bs)

Tactic:
disjoint_iff_ne

Goal state after:
case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ ∀ (a : List α), a ∈ permutations'Aux x as → ∀ (b : List α), b ∈ permutations'Aux x bs → a ≠ b
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
⊢ (if (x :: y :: tail).getLast hl = x then y else (y :: tail).nextOr ((x :: y :: tail).getLast hl) d) = d

Tactic:
split_ifs with h'

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : (x :: y :: tail).getLast hl = x
⊢ y = d

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : ¬(x :: y :: tail).getLast hl = x
⊢ (y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mp
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k ≤ Nat.log 2 (p ^ k)

Tactic:
calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)

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

Goal state before:
pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p

Tactic:
intro p hp
    rw [List.mem_append] at hp
    rcases hp with hp' | hp' <;> exact prime_of_mem_primeFactorsList hp'

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

Goal state before:
pp: case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(a + 1) = n / n.gcd (a + 1)

Tactic:
← Nat.smul_one_eq_cast,

Goal state after:
case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ((a + 1) • 1) = n / n.gcd (a + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf ↑a = n / n.gcd a

Tactic:
← Nat.smul_one_eq_cast,

Goal state after:
a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf (a • 1) = n / n.gcd a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n + 1 = 0

Tactic:
← Nat.cast_add_one,

Goal state after:
n : ℕ
⊢ ↑(n + 1) = 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
obtain (hH | hH) : H.index = 1 ∨ H.index = 2 := by
      -- This is just showing that 2 is prime, but we do it "longhand" to avoid making any
      -- dependence on number theory files.
      have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
      rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this
      exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim
    · simp [index_eq_one.mp hH]
    · exact match index_eq_two_iff.mp hH with | ⟨a, ha⟩ => ⟨a, fun b ↦ (ha b).or⟩

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

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Tactic:
← val_intCast,

Goal state after:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑(↑a).val
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ (stabilizer G x).index = Nat.card X

Tactic:
index_stabilizer,

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ (orbit G x).ncard = Nat.card X
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n ({d ∈ Ico 1 n | d ∣ n}) = if n ∣ n then insert n ({d ∈ Ico 1 n | d ∣ n}) else {d ∈ Ico 1 n | d ∣ n}

Tactic:
if_pos (dvd_refl n)

Goal state after:
n : ℕ
h : n ≠ 0
⊢ insert n ({d ∈ Ico 1 n | d ∣ n}) = insert n ({d ∈ Ico 1 n | d ∣ n})
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0

pp: case mpr
n a b : ℕ
⊢ a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b

Tactic:
· rintro ⟨han, ⟨ha, han'⟩, rfl⟩
    simp [Nat.mul_div_eq_iff_dvd, han]
    lia

Goal state after:
case mpr
n a b : ℕ
⊢ a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a * b).val = a.val * b.val % n

Tactic:
cases n
  · rw [Nat.mod_zero]
    apply Int.natAbs_mul
  · apply Fin.val_mul

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
obtain hx' | hx' := lt_or_ge x 0

Goal state after:
case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.divisors, i = 2 * n

Tactic:
sum_divisors_eq_sum_properDivisors_add_self,

Goal state after:
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = 2 * n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ range k, f (p ^ x)

Tactic:
simp [h, properDivisors_prime_pow]

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

Goal state before:
pp: case h.inl
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

pp: case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

pp: case h.inr.inr
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
· clear IH; exact False.elim ((not_lt.2 n_big) hn)

Goal state after:
case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

case h.inr.inr
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k = (p.maxPowDvdDiv n).fst

Tactic:
· apply Nat.le_antisymm
        · rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]
          apply Nat.le_refl
        · rw [← pow_dvd_iff_le_of_spec hp hn h hl, pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn]
          apply Nat.le_refl

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ zero ∣ b

Tactic:
rw [_root_.pow_zero]
        exact one_dvd _

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
← ENat.natCast_zero,

Goal state after:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑0 ↔ ¬a ∣ b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) ↑{L | L.length = l ∧ ∀ x ∈ L, x < b}.toFinset ↑(Finset.range (b ^ l))

Tactic:
Set.coe_toFinset

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} ↑(Finset.range (b ^ l))
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) ↑{L | L.length = l ∧ ∀ x ∈ L, x < b}.toFinset

Tactic:
Set.coe_toFinset

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) {L | L.length = l ∧ ∀ x ∈ L, x < b}
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p

Tactic:
← factorization_pow_self (n := n) hp

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ (p ^ n).factorization p ≤ ((p ^ n).choose k).factorization p + k.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
intro e hea heb
    rcases eq_or_ne e 0 with (rfl | he_pos)
    · exact absurd (zero_dvd_iff.mp hea) ha_pos
    apply dvd_prod_pow_of_factorization_le he_pos
    have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
    have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
    simp [hea', heb']

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)

Tactic:
push_cast
  rw [← emultiplicity_choose_prime_pow_add_emultiplicity hp hkn hk0,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, Nat.pos_of_ne_zero hk0⟩).emultiplicity_eq_multiplicity,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, choose_pos hkn⟩).emultiplicity_eq_multiplicity]
  norm_cast
  rw [Nat.add_sub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a : G
⊢ x * of' k G a /ᵒᶠ a = x

Tactic:
by
  ext; simp only [of'_apply, coeff_divOf, add_comm a, coeff_mul_single_add, mul_one]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n ∣ (∏ p ∈ n.primeFactors, p) ^ n

Tactic:
← Finset.prod_pow,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n ∣ ∏ x ∈ n.primeFactors, x ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝ : NonAssocRing R
n : ℕ
⊢ ↑n = 0 ↔ addOrderOf 1 ∣ n

Tactic:
← Nat.smul_one_eq_cast,

Goal state after:
R : Type u_6
inst✝ : NonAssocRing R
n : ℕ
⊢ n • 1 = 0 ↔ addOrderOf 1 ∣ n
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
⊢ X ^ (n + 1) ∣ f

Tactic:
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
⊢ X ^ (n + 1) ∣ f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

pp: case neg
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : ¬q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
· cases lt_or_ge (degree p) (degree q)
    · rw [(modByMonic_eq_self_iff hq).mpr ‹_›]
    · exact (degree_modByMonic_le p hq).trans ‹_›

Goal state after:
case neg
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : ¬q.Monic
⊢ (p %ₘ q).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ derivative ((monomial m) a * (monomial n) b) =
    derivative ((monomial m) a) * (monomial n) b + (monomial m) a * derivative ((monomial n) b)

Tactic:
| monomial n b =>

Goal state after:
case monomial.monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ derivative ((monomial m) a * (monomial n) b) =
    derivative ((monomial m) a) * (monomial n) b + (monomial m) a * derivative ((monomial n) b)
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 + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑m + 1) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)

Tactic:
← Nat.cast_add_one,

Goal state after:
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 + k).succ.descFactorial k • p.coeff (m + k.succ) * ↑(m + 1) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
⊢ False

Tactic:
have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
      hpq0 <|
        leadingCoeff_eq_zero.1
          (by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
by
        rw [Function.iterate_succ_apply', IH]

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

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

Tactic:
← modByMonic_X_sub_C_eq_C_eval,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ p %ₘ X = p %ₘ (X - C 0)
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 : 0 = p.coeff (m + 1) * (↑m + 1)
⊢ False

Tactic:
← Nat.cast_add_one,

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 : 0 = p.coeff (m + 1) * ↑(m + 1)
⊢ False
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
i : ↑I
⊢ eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)

Tactic:
exact preimage_mem_comap (h i i.2)

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
hq : q ≠ 0
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff

Tactic:
← leadingCoeff_ne_zero,

Goal state after:
K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
hq : q.leadingCoeff ≠ 0
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ T ∈ powersetCard (#S - k) S, derivative (∏ a ∈ T, (X - C a)) =
    ∑ T ∈ powersetCard (#S - k) S, ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)

Tactic:
congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
x : α
hx : x ∈ g
⊢ IsUnit g.prod

Tactic:
simpa [associated_one_iff_isUnit] using h.symm

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
⊢ ∃ p, p ∈ factors x

Tactic:
obtain ⟨p, hp, _⟩ := exists_mem_factors_of_dvd hx hp' hp'x

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ factors x
right✝ : p' ~ᵤ p
⊢ ∃ p, p ∈ factors x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ ↑(#S)
hp : p ≠ 0
⊢ S.val ≤ p.roots

pp: case refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ ↑(#S)
hp : p ≠ 0
⊢ p.roots.card ≤ S.val.card

Tactic:
· exact (Finset.val_le_iff_val_subset.mpr (fun x hx ↦ (p.mem_roots hp).mpr (hS x hx)))

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ ↑(#S)
hp : p ≠ 0
⊢ p.roots.card ≤ S.val.card
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
n : ℕ
⊢ (X ^ n).aroots S = n • {0}

Tactic:
aroots_pow,

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
n : ℕ
⊢ n • X.aroots S = n • {0}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
this : Fintype R
⊢ f = 0

Tactic:
apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero f Function.injective_id hf

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
this : Fintype R
⊢ f.natDegree < Fintype.card R
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬f.IsRoot a

Tactic:
rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : C (f.coeff 0) ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬(C (f.coeff 0)).IsRoot a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : (Multiset.map (fun a ↦ X - C a) p.roots).prod.roots + q.roots = p.roots
⊢ q.roots = 0

pp: case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).roots = p.roots
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod * q ≠ 0

Tactic:
roots_multiset_prod_X_sub_C

Goal state after:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : p.roots + q.roots = p.roots
⊢ q.roots = 0

case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).roots = p.roots
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod * q ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
⊢ p.roots.card ≤ 1

Tactic:
obtain hp | ⟨x, hx⟩ := p.roots.empty_or_exists_mem
  · simp [hp]
  convert! p.card_roots'
  exact (natDegree_eq_of_degree_eq_some <| degree_eq_one_of_irreducible_of_root hirr <|
    isRoot_of_mem_roots hx).symm

Goal state after: