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

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

Tactic:
digits_eq_cons_digits_div hb hn,

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

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

Tactic:
rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)

Goal state after:
case inl
m n : ℕ
hb : 0 < succ 0
⊢ (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)

case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ.isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : ¬FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ⊤
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
· apply FiniteMultiplicity.not_iff_forall.mp ‹_›

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

Goal state before:
pp: p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ (n + 1).factorization p ≤ ((n + 1).choose (k + 1)).factorization p + (k + 1).factorization p

Tactic:
rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos hkn)
      (zero_ne_add_one k).symm]
    refine factorization_le_factorization_of_dvd_right ?_ (zero_ne_add_one n).symm
      (Nat.mul_ne_zero (ne_of_gt <| choose_pos hkn) (by positivity))
    rw [← add_one_mul_choose_eq]
    exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
hk : x ^ k = 1
⊢ m + k ≡ m [MOD orderOf x]

Tactic:
by simpa using Nat.ModEq.add_left m (pow_eq_one_iff_modEq.1 hk)

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

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
subst hn

Goal state after:
case pos
⊢ ∏ p ∈ primeFactors 0, p ∣ 0
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)

Tactic:
by
  simpa using h.add_pow_prime_pow_eq' hp 1

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1

Tactic:
rw [ne_eq, ← isOfFinOrder_iff_eq_one, ← orderOf_eq_zero_iff] at ha

Goal state after:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : orderOf g = 0
⊢ orderOf g ≤ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∑ m ∈ n.divisors, #{x | orderOf x = m} = #{x | x ^ n = 1}

Tactic:
refine (Finset.card_biUnion ?_).symm.trans ?_

Goal state after:
case refine_1
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (↑n.divisors).PairwiseDisjoint fun m ↦ {x | orderOf x = m}

case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ #(n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = #{x | x ^ n = 1}
Module: Mathlib.Data.Nat.Multiplicity

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

Tactic:
subst hn

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ a.factorization p = b.factorization p

Tactic:
simp [factorization_def, pp, h p pp]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n = n

Tactic:
nth_rw 2 [← prod_factorization_pow_eq_self hn]

Goal state after:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n = n.factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) + ↑(p * (n / p)) = 0
⊢ p ∣ n

Tactic:
Nat.cast_mul,

Goal state after:
case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) + ↑p * ↑(n / p) = 0
⊢ p ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
H : ↑p = 0
n : ℕ
⊢ ↑(p * n) = 0

Tactic:
Nat.cast_mul,

Goal state after:
case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
H : ↑p = 0
n : ℕ
⊢ ↑p * ↑n = 0
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
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ X ^ (n + 1) ∣ f

Tactic:
use k

Goal state after:
case h
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
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ (n + 1) * k
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : (expand R n) g = (expand R n) g'
k : ℕ
⊢ g.coeff k = g'.coeff k

Tactic:
by rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p

Tactic:
let : Invertible a := ha.invertible

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
⊢ rootMultiplicity c (p.comp (C a * X + C b)) = rootMultiplicity (a * c + b) p

Tactic:
let : Invertible a := ha.invertible

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (p.comp (C a * X + C b)) = rootMultiplicity (a * c + b) p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
⊢ rootMultiplicity c (p.comp (C a * X + C b)) = rootMultiplicity (a * c + b) p

Tactic:
by
  let : Invertible a := ha.invertible
  apply le_antisymm (rootMultiplicity_comp_C_mul_X_add_C_le p a b c ha)
  have := rootMultiplicity_comp_C_mul_X_add_C_le
    (p.comp (C a * X + C b)) ⅟a (- ⅟a * b) (a * c + b) (isUnit_of_invertible ⅟a)
  simpa [comp_assoc, mul_add, ← mul_assoc, ← map_mul] using this

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : f.degree + g.degree = 1
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f

Tactic:
Nat.WithBot.add_eq_one_iff

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p /ₘ q = 0

Tactic:
have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold divByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]

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

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

Tactic:
exact add_le_add (le_refl (1 : WithBot ℕ)) htd

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalHom (expand R p)

Tactic:
by
  refine ⟨fun f hf1 => ?_⟩
  have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
  rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2
  rw [hf2, isUnit_C] at hf1; rw [expand_eq_C hp] at hf2; rwa [hf2, isUnit_C]

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

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

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

Tactic:
all_goals
  · apply dvd_mul_of_dvd_right
    simp [Polynomial.modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
ι' : ι → Type u_3
s : (i : ι) → ι' i → Set (α i)
p : (i : ι) → ι' i → Prop
h : ∀ (i : ι), (f i).HasBasis (p i) (s i)
⊢ (pi f).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If ↦ If.1.pi fun i ↦ s i (If.2 i)

Tactic:
by
  simpa [Set.pi_def] using! HasBasis.iInf' fun i => (h i).comap (eval i : (∀ j, α j) → α i)

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ t ∈ ⨅ a ∈ s, f a ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

Tactic:
classical
  simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

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

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree

Tactic:
rootMultiplicity_le_iff h,

Goal state after:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ¬(X - C 0) ^ (p.natTrailingDegree + 1) ∣ p
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
convert! (derivative^[2] p).iterate_derivative_mul_X_pow n 2

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n + 2] p * X ^ 2 + (2 * n) • (⇑derivative)^[n + 1] p * X + (n * (n - 1)) • (⇑derivative)^[n] p =
    ∑ k ∈ range (min 2 n).succ,
      (n.choose k * Nat.descFactorial 2 k) • ((⇑derivative)^[n - k] ((⇑derivative)^[2] p) * X ^ (2 - k))
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
Multiset.erase_cons_head,

Goal state after:
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ derivative (f i) * (Multiset.map f s).prod + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_3
α : Type u_2
f : Filter α
⊢ f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2

pp: case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
· rw [← compl_compl f.ker, ← hnot_principal, ← Filter.hnot_def,
      Coheyting.hnot_hnot_sup_boundary]

Goal state after:
case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
⊢ q = (f.ker, Coheyting.boundary f)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
hP' : derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
simp [hP']

Goal state after:
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
⊢ ↑k ! * ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑(k ! * (k + 1)) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
Nat.cast_mul,

Goal state after:
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
⊢ ↑k ! * ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑k ! * ↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
this : y.support ⊆ s
⊢ ↑y.support ⊆ range ⇑e

Tactic:
simpa [e]

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

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ {d | (weight w) d ≤ n}.Finite

Tactic:
by
  classical
  set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
  suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this
  intro d hd
  rw [hfg]
  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
  use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
  ext x
  dsimp at hd
  grw [← le_weight _ (hw x)] at hd
  simp [*]

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

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

Tactic:
rcases subsingleton_or_nontrivial α with h | h
  · dsimp [normalizedFactors, factors]
    simp [Subsingleton.elim (1 : α) 0]
  · rw [← Multiset.rel_zero_right]
    apply factors_unique irreducible_of_normalized_factor
    · intro x hx
      exfalso
      apply Multiset.notMem_zero x hx
    · apply prod_normalizedFactors one_ne_zero

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
hη₁ : η₁ ∈ nthRootsFinset n a₁
hη₂ : η₂ ∈ nthRootsFinset n a₂
⊢ η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂)

Tactic:
by
  cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη₁
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
    rw [mul_pow, hη₁, hη₂]

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

Goal state before:
pp: case neg.calc_1
α : 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
cne0 : c ≠ 0
con : Classical.choose ⋯ = 0
⊢ c ~ᵤ 1

Tactic:
convert! (Classical.choose_spec (pf c cne0)).2.symm

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
cne0 : c ≠ 0
con : Classical.choose ⋯ = 0
⊢ 1 = (Classical.choose ⋯).prod
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
p : T[X]
⊢ (-p).aroots S = p.aroots S

Tactic:
aroots,

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
⊢ (map (algebraMap T S) (-p)).roots = p.aroots S
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content ↔ C r ∣ p

Tactic:
rw [C_dvd_iff_dvd_coeff]
  constructor
  · intro h i
    apply h.trans (content_dvd_coeff _)
  · intro h
    rw [content, Finset.dvd_gcd_iff]
    intro i _
    apply h i

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

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
rcases h with ⟨b, rfl⟩
      obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b
      refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩
      · rw [mul_assoc, ha']
      · rw [mul_assoc, hb']

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

Goal state before:
pp: case neg.inl
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
⊢ IsUnit q

Tactic:
have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _

Goal state after:
case neg.inl
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
this : p ∣ c' * b'
⊢ IsUnit q
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ↑n ! ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
by
  by_contra! h'
  replace hroot := hroot _ h'
  simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot
  obtain ⟨q, hq⟩ : ((rootMultiplicity t p)! : R) ∣ n ! := by gcongr
  rw [hq, mul_mem_nonZeroDivisors] at hnzd
  rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot
  exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑((n + 1) * n !) ∈ nonZeroDivisors R

Tactic:
Nat.cast_mul,

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1) * ↑n ! ∈ nonZeroDivisors R
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
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b

Tactic:
classical
  have hz : factors (Associates.mk a) ⊓ factors (Associates.mk b) ≠ 0 := by
    contrapose h with hf
    change (factors (Associates.mk a) ⊓ factors (Associates.mk b)).prod = 1
    rw [hf]
    exact Multiset.prod_zero
  rw [factors_mk a ha, factors_mk b hb, ← WithTop.coe_inf] at hz
  obtain ⟨⟨p0, p0_irr⟩, p0_mem⟩ := Multiset.exists_mem_of_ne_zero ((mt WithTop.coe_eq_coe.mpr) hz)
  rw [Multiset.inf_eq_inter] at p0_mem
  obtain ⟨p, rfl⟩ : ∃ p, Associates.mk p = p0 := Quot.exists_rep p0
  refine ⟨p, ?_, ?_, ?_⟩
  · rw [← UniqueFactorizationMonoid.irreducible_iff_prime, ← irreducible_mk]
    exact p0_irr
  · apply dvd_of_mk_le_mk
    apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).left
    apply ha
  · apply dvd_of_mk_le_mk
    apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).right
    apply hb

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
hy : y ≠ 0
H : Type (max 0 u) := { x // x ∣ y }
⊢ Fintype G

Tactic:
let hfin : Fintype H := UniqueFactorizationMonoid.fintypeSubtypeDvd y hy

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
hy : y ≠ 0
H : Type (max 0 u) := { x // x ∣ y }
hfin : Fintype H := fintypeSubtypeDvd y hy
⊢ Fintype G
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Field R
p q : R[X]
inst✝ : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
⊢ Irreducible p ∧ normalize p = p ∧ p ∣ q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

Tactic:
normalize_eq_self_iff_monic hp

Goal state after:
case neg
R : Type u
inst✝¹ : Field R
p q : R[X]
inst✝ : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
⊢ Irreducible p ∧ p.Monic ∧ p ∣ q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
hx : IsAlgebraic K ↑x
⊢ (↑x)⁻¹ ∈ A

Tactic:
obtain ⟨p, ne_zero, aeval_eq⟩ := hx

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
ne_zero : p ≠ 0
aeval_eq : (aeval ↑x) p = 0
⊢ (↑x)⁻¹ ∈ A