mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList

Tactic:
· rintro ⟨c, rfl⟩
      rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb
      rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]
      exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
by_contra hc

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ¬∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ False
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
· exfalso
    exact m.succ_ne_zero h

Goal state after:
case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)

Tactic:
apply Fin.val_mul

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

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

Tactic:
rw [val_mul]
  apply Nat.mod_eq_of_lt h

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

Goal state before:
pp: n x : ℕ
h : x.gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
Nat.gcd_comm,

Goal state after:
n x : ℕ
h : n.gcd x = 1
⊢ ↑x * (↑x)⁻¹ = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.gcd n = 1

Tactic:
Nat.gcd_comm,

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ n.gcd m = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n

Tactic:
exact Nat.gcd_rec n m

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

Goal state before:
pp: p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ IsUnit ↑a ↔ ¬p ∣ a

Tactic:
rw [isUnit_iff_coprime, Nat.coprime_pow_right_iff hd, Nat.coprime_comm,
    hp.coprime_iff_not_dvd]

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

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.val x.cast.2.val) ≡ x.val [MOD m] ∧
    ↑(Nat.chineseRemainder h x.cast.val x.cast.2.val) ≡ x.val [MOD n]

Tactic:
Prod.snd_zmod_cast

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.val x.cast.val) ≡ x.val [MOD m] ∧
    ↑(Nat.chineseRemainder h x.cast.val x.cast.val) ≡ x.val [MOD n]
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
rw [mul_zero, mul_eq_zero] at he

Goal state after:
case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 = 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)

Tactic:
· apply Nat.succ_pos

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

Goal state before:
pp: m n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
⊢ (a ^ m).val ≤ a.val ^ m

Tactic:
by
  induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    rw [pow_succ, pow_succ]
    apply le_trans (ZMod.val_mul_le _ _)
    apply Nat.mul_le_mul_right _ ih

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

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ (↑n * m + x).natAbs

Tactic:
← add_le_add_iff_right x.natAbs

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + x.natAbs ≤ (↑n * m + x).natAbs + x.natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
⊢ f = g

Tactic:
ext a
  obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a
  let φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
  let ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
  change φ k = ψ k
  rw [φ.ext_int ψ]

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

Goal state before:
pp: case ind.succ
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits (n + 1)
⊢ d < b + 2

Tactic:
rw [digits_add_two_add_one] at hd

Goal state after:
case ind.succ
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
⊢ d < b + 2
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]

Goal state after:
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
⊢ 0 = ofDigits 0 L - L.sum
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inr
p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
simp [lt_one_iff.mp h]

Goal state after:
case inr.inr
p n : ℕ
h : p < 1
⊢ 0 = n - (digits 0 n).sum
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : emultiplicity a b < ↑m
nh : a ^ m ∣ b
⊢ False

Tactic:
unfold emultiplicity at hm

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) < ↑m
nh : a ^ m ∣ b
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
k : α
hk : c = a * k
⊢ False

Tactic:
rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc

Goal state after:
α : 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
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ (∃ n, 0 < n ∧ a ^ n = 1) → ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1

Tactic:
rintro ⟨m, hm, ha⟩

Goal state after:
G : Type u_1
inst✝ : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a : ℕ
b : ℤ
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

Tactic:
rcases Int.natAbs_eq b with h | h

Goal state after:
case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p n.primeFactorsList) p
⊢ count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList

Tactic:
simp [List.eq_of_mem_replicate hq]

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

Goal state before:
pp: k x p : ℕ
hp : Prime p
hx : p ^ k ∣ x
⊢ x / p ^ k / p ^ (x / p ^ k).factorization p = x / p ^ x.factorization p

Tactic:
obtain ⟨m, rfl⟩ := hx
  rw [Nat.mul_div_cancel_left m (pow_pos hp.pos k), ← ordCompl_self_pow_mul m k hp]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G₀ : Type u_6
inst✝¹ : GroupWithZero G₀
inst✝ : Finite G₀
a : G₀
this : Finite G₀ˣ
⊢ orderOf a = 0 ↔ a = 0

Tactic:
simp [isOfFinOrder_iff_isUnit]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)

Tactic:
exact dvd_add h₁ (h₂.trans <| (dvd_mul_right ..).trans <| dvd_mul_right ..)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1

Tactic:
by
  obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x
  refine ⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩
  rw [zpow_natCast]
  exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2

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

Goal state before:
pp: case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ p ^ n.factorization p = 1

Tactic:
simp [Finsupp.notMem_support_iff.mp hp2]

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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)
    rwa [zpow_add, zpow_mul, zpow_mul', zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one,
      pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ c ∣ p ^ n

Tactic:
← CharP.cast_eq_zero_iff R c,

Goal state after:
R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ ↑(p ^ n) = 0
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
coeff_expand_mul hp

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ f.coeff n = f.coeff n
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]
a : R
p : R[X]
⊢ (p.sum fun n a_1 ↦ C (a * a_1 * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
simp only [mul_sum, ← C_mul', mul_assoc, map_mul, forall_const, zero_mul, map_zero, sum]

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

Goal state before:
pp: case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
a : R
p : R[X]
⊢ ∀ (i : ℕ), C (0 * ↑i) * X ^ (i - 1) = 0

Tactic:
simp only [mul_sum, ← C_mul', mul_assoc, map_mul, forall_const, zero_mul, map_zero, sum]

Goal state after:
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).coeff (f.natDegree * p) = f.coeff f.natDegree

Tactic:
coeff_expand_mul hp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝

Tactic:
dvd_iff_isRoot,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ (x✝¹ * x✝).IsRoot r → x✝¹.IsRoot r ∨ x✝.IsRoot r
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:
rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬X - C (r ^ p ^ n) ∣ g
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
dvd_iff_isRoot,

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬g.IsRoot (r ^ p ^ n)
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ 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
⊢ (Multiset.map (⇑(aeval x)) (Multiset.map (fun x ↦ X - C x) s)).prod = 0

Tactic:
Multiset.prod_eq_zero

Goal state after:
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
⊢ 0 = 0

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
⊢ 0 ∈ Multiset.map (⇑(aeval x)) (Multiset.map (fun x ↦ X - C x) s)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
rw [Icc_eq_empty (Nat.lt_succ_iff.mpr h).not_ge, sum_empty]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = 0
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
dvd_iff_isRoot,

Goal state after:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
⊢ (p - C (eval a p)).IsRoot a
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
⊢ (C ↑n * p ^ n * p + C 1 * p ^ n * p) * derivative p + p ^ n * p * derivative p =
    C (↑n.succ + 1) * p ^ n * p * derivative p

Tactic:
C_1,

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨆ i, f i).ker = ⋃ i, (f i).ker

Tactic:
by
  refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup
  simp only [mem_iUnion, mem_ker] at hx ⊢
  contrapose! hx
  choose s hsf hxs using hx
  refine ⟨⋃ i, s i, ?_, by simpa⟩
  exact mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

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

Goal state before:
pp: 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)

pp: 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)

Tactic:
· simpa [hi] using image_mem_map (hs i hi)

Goal state after:
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.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst✝² : AddCommMonoid M
inst✝¹ : TendstoCofinite f
inst✝ : DistribSMul R M
r : R
v : α → M
⊢ mapDomain f (r • v) = r • mapDomain f v

Tactic:
by ext; simp [mapDomain, Finset.smul_sum]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ~ᵤ g i
⊢ ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i

Tactic:
induction s using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    rfl
  | insert j s hjs IH =>
    classical
    convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
    grind [Associated.mul_mul]

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

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

Tactic:
rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, hc⟩

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

case cons.inr.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hc : y = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
simp only [notMem_support_iff] at h
    rw [h]
    apply zero_le

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
rw [← count_pos, count_roots p, rootMultiplicity_pos']

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

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

Tactic:
have hf : Function.Bijective f :=
    (AddGroup.addRight_bijective b).comp (IsUnit.isUnit_iff_mulLeft_bijective.mp ha)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
⊢ Multiset.map f (p.comp (C a * X + C b)).roots = p.roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C 1 * X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}

Tactic:
C_1,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (1 * X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n 1
f : F
⊢ f x ∈ nthRootsFinset n 1

Tactic:
← (map_one f)

Goal state after:
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n 1
f : F
⊢ f x ∈ nthRootsFinset n (f 1)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.content = (Finset.range n).gcd p.coeff

Tactic:
apply dvd_antisymm_of_normalize_eq normalize_content Finset.normalize_gcd

Goal state after:
case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.content ∣ (Finset.range n).gcd p.coeff

case hba
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (Finset.range n).gcd p.coeff ∣ p.content