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

Goal state before:
pp: p✝ n p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ 1 < p * p ∧ n ≠ 0

Tactic:
by simp [Nat.one_lt_mul_iff, hp, Nat.lt_trans Nat.one_pos]

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

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

pp: case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
· simp [h]
    aesop

Goal state after:
case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b n : ℕ
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  rcases le_or_gt b 1 with hb | hb
  · interval_cases b <;> simp +arith [digits_zero_succ', hn]
  simpa [length_digits, hb, hn] using log_mono_right (le_succ _)

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)

Tactic:
simp only [ofDigits, add_sub_add_left_eq_sub]

Goal state after:
case cons
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ a * ofDigits a L - b * ofDigits b L
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
by
  constructor
  · intro h
    constructor
    · apply pow_dvd_of_le_emultiplicity
      simp [h]
    · apply not_pow_dvd_of_emultiplicity_lt
      rw [h]
      norm_cast
      simp
  · rw [and_imp]
    apply emultiplicity_eq_of_dvd_of_not_dvd

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ p ^ a✝ ∣ a + b

Tactic:
simp [dvd_add, pow_dvd_of_le_emultiplicity, ← hm]

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

Goal state before:
pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
⊢ x ∈ S →
    T ⊆ S →
      x ∉ T →
        (T.prod g).factorization = ∑ x ∈ T, (g x).factorization →
          ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization

Tactic:
hxS

Goal state after:
case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
⊢ T ⊆ S →
    x ∉ T →
      (T.prod g).factorization = ∑ x ∈ T, (g x).factorization →
        ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
key : x ^ (2 * (r + 1)) = x
⊢ ∃ m, x ^ n = x ^ (2 * m)

Tactic:
exact ⟨(r + 1) * n, by rw [← mul_assoc, pow_mul, key]⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a = a ^ 2 * v
⊢ False

Tactic:
nth_rw 1 [← mul_one a] at hv

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = a ^ 2 * v
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization p = ∑ x ∈ S, (g x).factorization p

Tactic:
factorization_prod hS,

Goal state after:
α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (∑ x ∈ S, (g x).factorization) p = ∑ x ∈ S, (g x).factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
⊢ orderOf (x ^ n) = orderOf x / n

Tactic:
by rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]

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

Goal state before:
pp: case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ p ^ d.factorization p ∣ n

Tactic:
exact h p _ pp (ordProj_dvd _ _)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ (closure s).toSubmonoid = Submonoid.closure s

Tactic:
refine le_antisymm ?_ (le_closure_toSubmonoid s)
  rw [closure_toSubmonoid]
  refine Submonoid.closure_le.mpr <| Set.union_subset Submonoid.subset_closure
    fun x (hx : x⁻¹ ∈ s) ↦ ?_
  apply Submonoid.powers_le.mpr (Submonoid.subset_closure hx)
  simp [(hs _ hx).mem_powers_iff_mem_zpowers]

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

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

Tactic:
prime_two.emultiplicity_factorial_mul

Goal state after:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(2 * n)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ¬p = C (p.coeff 0)

Tactic:
exact fun h0 => h (h0.symm ▸ degree_C_le)

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity y (X - C y) = 1

Tactic:
exact rootMultiplicity_X_sub_C_self

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
this : r.natDegree = 0
⊢ p * C (r.coeff 0) = p * C (p * C (r.coeff 0)).leadingCoeff

Tactic:
simp [leadingCoeff_monic_mul hp]

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

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

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

pp: case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n + 1 ∉ p.support → (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0

Tactic:
· simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true]; norm_cast

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

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n + 1 ∉ p.support → (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ p.coeff (n✝ + 1) * ↑(n✝ + 1) * 0 = 0

Tactic:
mul_zero

Goal state after:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case hp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ (C a * X + C b).degree = 1

Tactic:
compute_degree!

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ f.coeff (x, y).1 * 0 = 0

Tactic:
mul_zero

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
have hp : p ≠ 0 := left_ne_zero_of_mul hpq
  have hq : q ≠ 0 := right_ne_zero_of_mul hpq
  rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]

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]
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hp : (X - C x) * 0 ≠ 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
mul_zero

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hp : 0 ≠ 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False
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
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a p

Tactic:
conv_rhs => rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]

Goal state after:
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
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a ((X - C x) * (p /ₘ (X - C x)))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: 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 : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((expand R (p ^ n)) (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * (expand R (p ^ n)) g)

Tactic:
map_sub,

Goal state after:
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 : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r
    (((expand R (p ^ n)) X - (expand R (p ^ n)) (C (r ^ p ^ n))) ^ rootMultiplicity (r ^ p ^ n) f *
      (expand R (p ^ n)) g)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
rw [expand_eq_C hp] at hf2

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case neg.a
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
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree ≤ q.natDegree

Tactic:
compute_degree!

Goal state after:
case neg.a.a
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
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ q.natDegree - p.natDegree + p.natDegree ≤ q.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p * q %ₘ q = 0

Tactic:
by
  rw [modByMonic_eq_zero_iff_dvd hq]
  exact dvd_mul_left q p

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

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

Tactic:
induction k with
  | zero => simp
  | succ k IH =>
      simp [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_X_add_C_pow]
      ring

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

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

Tactic:
Finset.set_biInter_insert,

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ s ∈ f i

Tactic:
refine mem_of_superset (htf i) ((subset_eval_image_pi ?_ _).trans hI)

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ (I.pi t).Nonempty
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢(a ⊓ ￢a) = ⊤

Tactic:
hnot_inf_distrib,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢a ⊔ ￢￢a = ⊤
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
hnot_inf_distrib,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ b ⊓ (￢a ⊔ ￢b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
s t : Set (Multiplicative M)
⊢ ⇑toAdd '' (s * t) = ⇑toAdd '' s + ⇑toAdd '' t

Tactic:
rw [← Set.image2_mul, Set.image_image2_distrib toAdd_mul, Set.image2_add]

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = (weight w) f

Tactic:
conv_rhs => rw [← sub_add_single_one_cancel hi, weight_apply]

Goal state after:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = (f - single i 1 + single i 1).sum fun i c ↦ c • w i
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ normalizedFactors 1 = 0

Tactic:
dsimp [normalizedFactors, factors]

Goal state after:
case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ Multiset.map normalize (if h : 1 = 0 then 0 else Classical.choose ⋯) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬normalizedFactors x = 0 ↔ ¬IsUnit x

Tactic:
← normalizedFactors_pos _ hx,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬normalizedFactors x = 0 ↔ 0 < normalizedFactors x
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hp : IsPrimitive 0
⊢ False

Tactic:
exact (hp 0 (dvd_zero (C 0))).ne_zero rfl

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

Goal state before:
pp: case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
hc : c = 0
⊢ p.prod * 0 = 0

Tactic:
mul_zero

Goal state after:
case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
hc : c = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
con : c = 0
⊢ a * 0 = 0

Tactic:
mul_zero

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
con : c = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i

Tactic:
rw [eraseLead_coeff, if_neg hi.1]

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

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

Tactic:
mul_zero

Goal state after:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ (gcd p (derivative p)).IsRoot t

Tactic:
one_lt_rootMultiplicity_iff_isRoot h,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ p.IsRoot t ∧ (derivative p).IsRoot t ↔ (gcd p (derivative p)).IsRoot t
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, a.factors = ↑s) ↔ a ≠ 0

Tactic:
by
  simp_rw [@eq_comm _ a.factors, ← WithTop.ne_top_iff_exists]
  exact factors_eq_top_iff_zero.not

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ C q.leadingCoeff⁻¹ * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ (mapRingHom f) (X - C a) ^ rootMultiplicity a p

Tactic:
map_sub,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ ((mapRingHom f) X - (mapRingHom f) (C a)) ^ rootMultiplicity a p
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 * q.content) * (p.primPart * q.primPart)

Tactic:
map_mul

Goal state after:
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)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p0 : Associates α
p0_irr : Irreducible p0
p0_mem : ⟨p0, p0_irr⟩ ∈ factors' a ⊓ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b

Tactic:
Multiset.inf_eq_inter

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p0 : Associates α
p0_irr : Irreducible p0
p0_mem : ⟨p0, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ Irreducible (Associates.mk p)

Tactic:
exact p0_irr

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

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = ↑0
unit_c : IsUnit c.leadingCoeff
⊢ C c.leadingCoeff = C (c.coeff 0)

Tactic:
Polynomial.leadingCoeff,

Goal state after:
case right
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = ↑0
unit_c : IsUnit c.leadingCoeff
⊢ C (c.coeff c.natDegree) = C (c.coeff 0)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k = (Multiset.map Subtype.val (replicate k ⟨p, hp⟩)).prod

Tactic:
rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ p.count (a ^ k).factors

Tactic:
rw [count_pow ha hp]

Goal state after:
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ k * p.count a.factors