mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ f.ker.index = Nat.card ↥f.range

Tactic:
rw [← MonoidHom.comap_bot, index_comap, relIndex_bot_left]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero n
a : ZMod n
⊢ a.cast = ↑a.val

Tactic:
by
  cases n
  · cases NeZero.ne 0 rfl
  rfl

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero n
⊢ Nat.cast ∘ val = cast

Tactic:
by
  cases n
  · cases NeZero.ne 0 rfl
  rfl

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = a * a⁻¹ + ↑n.succ * ↑(a.val.gcdB n.succ)

Tactic:
by
        rw [natCast_self, zero_mul, add_zero]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisorsAntidiagonal 1 = {(1, 1)}

Tactic:
ext
  simp [mul_eq_one, Prod.ext_iff]

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

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

Tactic:
rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n

pp: case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n

Tactic:
· rw [h]

Goal state after:
case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.zero
⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ↔ Prime (0 + 1)

pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Tactic:
· simp [Nat.not_prime_one]

Goal state after:
case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [h, divisors_prime_pow]

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

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i ∈ range 0, a / b ^ i) * (b - 1) ≤ a * b

pp: case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b

Tactic:
· rw [sum_range_zero, zero_mul]
    exact Nat.zero_le _

Goal state after:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x z : ℤ
⊢ x ∈ z.divisors ↔ x ∣ z ∧ z ≠ 0

Tactic:
simp [mem_divisors_iff_natAbs_mem_divisors_natAbs]

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

Goal state before:
pp: case inl
n k : ℕ
h : k ≤ n
⊢ n.choose k ≤ (n + 1 - k) ^ k

pp: case inr
n k : ℕ
h : n < k
⊢ n.choose k ≤ (n + 1 - k) ^ k

Tactic:
· obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le h
    rw [Nat.add_comm k m, Nat.add_right_comm, Nat.add_sub_cancel]
    exact choose_add_le_add_one_pow m k

Goal state after:
case inr
n k : ℕ
h : n < k
⊢ n.choose k ≤ (n + 1 - k) ^ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ 2 * a.val

Tactic:
· rw [h]

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

Goal state before:
pp: ⊢ ∀ (n : ℕ), n.centralBinom < (n + 1).centralBinom

Tactic:
by grind [Nat.choose_pos, centralBinom]

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

Goal state before:
pp: n : ℕ
⊢ (2 * n + 1).choose n * (2 * n + 2) = 2 * ((2 * n + 1).choose n * (n + 1))

Tactic:
ring

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

Goal state before:

Tactic:
4 ^ (n + 1)
    _ = 4 * 4 ^ n := by rw [pow_succ']
    _ < 4 * (n * centralBinom n) := by gcongr; exact IH n n.lt_succ_self (Nat.le_of_lt_succ hn)
    _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
    _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm

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

Goal state before:
pp: case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2

Tactic:
ring

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

Goal state before:
pp: case succ.zero.succ
n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (n + 1)) = n + 1

Tactic:
simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]

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

Goal state before:
pp: case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1

Tactic:
simp only [digits_add_two_add_one]

Goal state after:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((n✝ + 1) % (b + 2) :: (b + 2).digits ((n✝ + 1) / (b + 2))) = n✝ + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)

Tactic:
ring

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

Goal state before:
pp: case e_f
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * b ^ (x✝ + 1) = b * (x✝¹ * b ^ x✝)

Tactic:
ring

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

Goal state before:
pp: b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b ^ (b.digits n).length * (b ^ k * m) = b ^ ((b.digits n).length + k) * m

Tactic:
ring

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

Goal state before:
pp: case inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

pp: case inr.inr
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
· interval_cases b <;> simp +arith [digits_zero_succ', hn]

Goal state after:
case inr.inr
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
apply Nat.div_lt_self

Goal state after:
case ind.succ.tail.a.hLtN
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 0 < n + 1

case ind.succ.tail.a.hLtK
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 1 < b + 2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.cons.hab
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd < p

Tactic:
exact w₁ hd List.mem_cons_self

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ∃ m_1 < m, ¬a ^ (m_1 + 1) ∣ b
⊢ False

Tactic:
obtain ⟨n, hn1, hn2⟩ := hm

Goal state after:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
n : ℕ
hn1 : n < m
hn2 : ¬a ^ (n + 1) ∣ b
⊢ False
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: a b : ℕ
t : List ℕ
⊢ ↑a + -1 * (↑b + -1 * (List.map (fun n ↦ ↑n) t).alternatingSum) = ↑a + -↑b + (List.map (fun n ↦ ↑n) t).alternatingSum

Tactic:
ring

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

Goal state before:
pp: case refine_1
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n

Tactic:
rw [← prod_factorization_pow_eq_self hn, ← prod_factorization_pow_eq_self hd]
    exact prod_dvd_prod_of_subset_of_dvd (support_mono hdn) fun a _ ↦ pow_dvd_pow a (hdn a)

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

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

Tactic:
ring

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

Goal state before:
pp: case succ
p : ℕ
hp : Prime p
n : ℕ
ih : (p * n)!.factorization p = n !.factorization p + n
⊢ n !.factorization p + n + (n + 1).factorization p + 1 = (n + 1).factorization p + n !.factorization p + (n + 1)

Tactic:
ring

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

Goal state before:
pp: n k p : ℕ
hp : Prime p
⊢ p ^ k * n / p ^ (p ^ k * n).factorization p = n / p ^ n.factorization p

Tactic:
ordCompl_mul,

Goal state after:
n k p : ℕ
hp : Prime p
⊢ p ^ k / p ^ (p ^ k).factorization p * (n / p ^ n.factorization p) = n / p ^ n.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ orderOf (-1) = if ringChar R = 2 then 1 else 2

Tactic:
split_ifs with h
  · rw [neg_one_eq_one_iff.2 h, orderOf_one]
  apply orderOf_eq_prime
  · simp
  simpa [neg_one_eq_one_iff] using h

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

Goal state before:
pp: ⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n

Tactic:
have h2 := prime_two.prime
  refine binaryRec ?_ ?_
  · exact fun h => False.elim <| h rfl
  · intro b n ih h
    by_cases hn : n = 0
    · subst hn
      simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h
      simp only [bit, h, cond_true, mul_zero, zero_add, factorial_one]
      rw [Prime.emultiplicity_one]
      · exact zero_lt_one
      · decide
    have : emultiplicity 2 (2 * n)! < (2 * n : ℕ) := by
      rw [prime_two.emultiplicity_factorial_mul]
      rw [two_mul]
      push_cast
      apply WithTop.add_lt_add_right _ (ih hn)
      exact Ne.symm nofun
    cases b
    · simpa
    · suffices emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
        simpa [emultiplicity_mul, h2, prime_two, bit, factorial]
      rw [emultiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
      refine this.trans ?_
      exact mod_cast lt_succ_self _

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (X * p.divX + C (p.coeff 0)).coeff 0 = p.coeff 0

Tactic:
simp [coeff_C]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (X * p.divX + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)

Tactic:
simp [coeff_C]

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

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases ha0 : a = 0
  · symm at h
    by_cases hm0 : m = 0
    · simp_all
    · use 0
      simp_all
  by_cases hn0 : n = 0
  · use b
    simp_all
  let factors := a.factorization.mapRange (· / n) (Nat.zero_div n)
  set c := factors.prod (· ^ ·) with hc
  use c
  suffices ha : a = c ^ n by
    refine ⟨ha, ?_⟩
    apply Nat.pow_left_injective hn0
    simp [← h, ha, Nat.pow_right_comm]
  apply eq_of_factorization_eq ha0 (by simp [c, factors])
  intro p
  have foo (p) (hp : p ∈ factors.support) : Prime p :=
    prime_of_mem_primeFactors (Finsupp.support_mapRange hp)
  rw [factorization_pow, hc, prod_pow_factorization_eq_self foo]
  suffices n ∣ a.factorization p by
    simp [factors, Nat.mul_div_cancel' this]
  refine hmn.symm.dvd_of_dvd_mul_left ⟨b.factorization p, ?_⟩
  simpa using congr(factorization $h p)

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).natDegree ≤ df + dg

Tactic:
exact natDegree_mul_le_of_le ‹_› ‹_›

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
    trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(p.natTrailingDegree + q.natTrailingDegree) = ↑p.natTrailingDegree + ↑q.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (((monomial n) a).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = (monomial (n - 1)) (a * ↑n)

Tactic:
sum_monomial_index,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (a * ↑n) * X ^ (n - 1) = (monomial (n - 1)) (a * ↑n)

case hf
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative ((monomial (n + 1)) a) = (monomial n) (a * (↑n + 1))

Tactic:
by
  rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]

Goal state after:
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
hq : ¬q.Monic
⊢ p = p - q * (p /ₘ q)

Tactic:
divByMonic_eq_of_not_monic _ hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p = p - q * 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p q : R[X]
h : ¬q.Monic
⊢ q ∣ p %ₘ q - p

Tactic:
· simp [modByMonic_eq_of_not_monic, h]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C (a ^ p) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p

Tactic:
ring

Goal state after:
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
⊢ (p /ₘ q).degree < p.degree

Tactic:
divByMonic_eq_of_not_monic _ hq,

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
⊢ degree 0 < p.degree
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : p = 0
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
convert! hq
    simp [hp, cancelLeads]

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

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

Tactic:
ring

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

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

Tactic:
ring

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

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

Tactic:
ring

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ (⇑derivative)^[n] (derivative (derivative (derivative (derivative p)))) * X ^ 2 +
        (2 * (n + 1 + 1)) • (⇑derivative)^[n] (derivative (derivative (derivative p))) * X +
      ((n + 1 + 1) * (n + 1)) • (⇑derivative)^[n] (derivative (derivative p)) =
    (⇑derivative)^[n] (derivative (derivative (derivative (derivative p)))) * X ^ 2 +
        ((n + 1 + 1) * 2) • ((⇑derivative)^[n] (derivative (derivative (derivative p))) * X) +
      ((n + 1 + 1) * (n + 1)) • (⇑derivative)^[n] (derivative (derivative p))

Tactic:
ring

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

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ C a✝ * (↑n✝ * q ^ (n✝ - 1) * derivative q) = derivative q * (C a✝ * ↑n✝ * q ^ (n✝ - 1))

Tactic:
ring

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine le_sup_of_le_right ?_
    rw [hnot_le_iff_codisjoint_right]
    exact codisjoint_hnot_right.mono_right (hnot_anti inf_le_left)

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a

Tactic:
exact hnot_hnot_le

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

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

Tactic:
rw [prod_eq, seq_pure, map_map]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ map ((fun g ↦ g b) ∘ Prod.mk) f = map (fun a ↦ (a, b)) f
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ ((∃ x, ↑x = ∅) ∨ ∃ x, ↑x = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g

Tactic:
Subtype.exists,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ ((∃ a, ∃ (_ : a ∈ f), a = ∅) ∨ ∃ a, ∃ (_ : a ∈ g), a = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ (normalizedFactors x + normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod

Tactic:
rw [Multiset.prod_add]
    exact
      ((prod_normalizedFactors hx).mul_mul (prod_normalizedFactors hy)).trans
        (prod_normalizedFactors (mul_ne_zero hx hy)).symm

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

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ 0 = (n + 1) • 0

Tactic:
smul_zero

Goal state after:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ a ∣ b ∧ b ∣ a

Tactic:
exact Associated.dvd_dvd h

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : NormalizedGCDMonoid R
S : Type u_2
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
inst✝¹ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
inst✝ : Nontrivial S
⊢ (algebraMap R S) p.content ≠ 0

Tactic:
have : IsDomain R := { Module.nontrivial R S with }

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : NormalizedGCDMonoid R
S : Type u_2
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
inst✝¹ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
inst✝ : Nontrivial S
this : IsDomain R
⊢ (algebraMap R S) p.content ≠ 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ p.coeff x - q.coeff x = a * w.coeff x

Tactic:
rw [← coeff_sub, hw, coeff_C_mul]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b • 0 = 0

Tactic:
smul_zero

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (Multiset.map (fun a ↦ X - C a) (replicate (count r s) r)).prod ∣ p

Tactic:
← Multiset.filter_eq

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (Multiset.map (fun a ↦ X - C a) (Multiset.filter (Eq r) s)).prod ∣ p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : FactorSetMem s p
⊢ False

Tactic:
FactorSetMem,

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : if hp : Irreducible p then BfactorSetMem ⟨p, hp⟩ s else False
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a ↦ X - C a) (replicate (count b (Multiset.map (⇑f) p.roots)) b)).prod ∣ map f p

Tactic:
← Multiset.filter_eq

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a ↦ X - C a) (Multiset.filter (Eq b) (Multiset.map (⇑f) p.roots))).prod ∣ map f p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
⊢ a.prod ≤ b.prod ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, prod_mono⟩

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
⊢ a ≤ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
this : a.prod.factors ≤ b.prod.factors
⊢ a ≤ b

Tactic:
rwa [prod_factors, prod_factors] at this

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C p.content * p.primPart * (C q.content * q.primPart) = C p.content * C q.content * (p.primPart * q.primPart)

Tactic:
ring

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

Goal state before:
pp: R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ ((C ((↑u).coeff 0)).coeff n)⁻¹ = (↑u⁻¹).coeff n

Tactic:
eq_C_of_degree_eq_zero (degree_coe_units u⁻¹),

Goal state after:
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ ((C ((↑u).coeff 0)).coeff n)⁻¹ = (C ((↑u⁻¹).coeff 0)).coeff n