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

Goal state before:
pp: case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ 0 :: (List.replicate k 0 ++ b.digits m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
List.replicate_succ,

Goal state after:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ 0 :: (List.replicate k 0 ++ b.digits m) = 0 :: List.replicate k 0 ++ b.digits m
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hk.h₁
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a

pp: case h₂
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ b

Tactic:
· apply pow_dvd_of_le_emultiplicity
      exact h.le

Goal state after:
case h₂
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
pp : ¬Prime p
⊢ 0 < p ^ n.factorization p

Tactic:
simp [pp]

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

Goal state before:
pp: n p : ℕ
hn : ¬n = 0
pp : ¬Prime p
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
simp [pp]

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

Goal state before:
pp: p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i =
    ∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0)

Tactic:
by
      simp only [Nat.add_div (pow_pos hp.pos _)]

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

Goal state before:
pp: case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n

Tactic:
rintro (n_eq_zero | not_dvd)
    · simp [n_eq_zero]
    · simp [Nat.factorization_eq_zero_of_not_dvd not_dvd]

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

Goal state before:
pp: case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
simp [pp]

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

Goal state before:
pp: n : ℕ
⊢ ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p = n.centralBinom

Tactic:
apply prod_pow_factorization_choose
  lia

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Injective fun n ↦ x ^ n
⊢ IsOfFinOrder x

Tactic:
rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Injective fun n ↦ x ^ n
⊢ IsOfFinOrder x

Tactic:
rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 ^ p = 0

Tactic:
← add_pow_expChar_of_commute _ (Commute.one_right _),

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1 + 1) ^ p = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
⊢ IsMulTorsionFree G

Tactic:
refine ⟨fun n hn a b hab ↦ ?_⟩

Goal state after:
G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)

Tactic:
induction n with
  | zero => simp [hp.emultiplicity_one]
  | succ n h =>
    rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.natCast_add]

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

Goal state before:
pp: case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
primeFactors_mul hm₀ hn₀,

Goal state after:
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ M p

Tactic:
by
    have wf : degree (divX p) < degree p := degree_divX_lt hp
    rw [← divX_mul_X_add p] at *
    exact
      if hcp0 : coeff p 0 = 0 then by
        rw [hcp0, C_0, add_zero]
        exact
          MX _ (fun h : divX p = 0 => by simp [h, hcp0] at hp) (recOnHorner (divX p) M0 MC MX)
      else
        MC _ _ (coeff_mul_X_zero _) hcp0
          (if hpX0 : divX p = 0 then show M (divX p * X) by rw [hpX0, zero_mul]; exact M0
          else MX (divX p) hpX0 (recOnHorner _ M0 MC MX))

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

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

Tactic:
simp only [coeff_X_pow, coeff_sum, coeff_C_mul]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun a b ↦ b * ↑a * if n = a - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ eval r x✝¹ * eval r x✝ = 0 → eval r x✝¹ = 0 ∨ eval r x✝ = 0

Tactic:
mul_eq_zero

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ eval r x✝¹ = 0 ∨ eval r x✝ = 0 → eval r x✝¹ = 0 ∨ eval r x✝ = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree + 1 ≤ n * 1

Tactic:
simpa only [mul_one] using hn

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p

Tactic:
by
  simp_rw [← smul_eq_C_mul, iterate_derivative_smul]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
natDegree_lt_natDegree_iff hp'

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).degree < p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)

Tactic:
by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
⊢ p %ₘ q = 0

Tactic:
obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
⊢ p %ₘ q = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    k ! • ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x

Tactic:
smul_sum

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    ∑ x ∈ ((⇑derivative)^[k] p).support, k ! • (C ((x + k).choose k • p.coeff (x + k)) * X ^ x)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
r a : R
⊢ rootMultiplicity a (C r) = 0

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a (C r) = 0

case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ rootMultiplicity a (C r) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) i = (Finsupp.single 0 X + Finsupp.single 1 1) i

Tactic:
match i with
  | 0 => simp
  | 1 => simp
  | (n + 2) => simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
⊢ s i ∈ f i

Tactic:
refine mem_of_superset (htf i) fun x hx => ?_

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
⊢ x ∈ s i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ x, f ↑x ≤ᶠ[l] ⋃ i ∈ s, g i

Tactic:
biUnion_eq_iUnion

Goal state after:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ x, f ↑x ≤ᶠ[l] ⋃ x, g ↑x
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ {x | p x}.Infinite

Tactic:
by
  simp only [Filter.Frequently, eventually_cofinite, not_not, Set.Infinite]

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

Goal state before:
pp: case cons
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, y ∈ {r | IsUnit r ∨ Prime r}) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ c ::ₘ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : (c ::ₘ s).prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
simp only [Multiset.mem_cons, forall_eq_or_imp, Set.mem_ofPred] at hm
    simp only [Multiset.prod_cons] at hprod
    simp only [Set.mem_ofPred_eq] at hind
    obtain ⟨ha₁ | ha₂, hs⟩ := hm
    · rcases ha₁.exists_right_inv with ⟨k, hk⟩
      refine hind x (y * k) ?_ hs ?_
      · simp only [← mul_assoc, ← hprod, ← Multiset.prod_cons, mul_comm]
        refine multiset_prod_mem _ _ (Multiset.forall_mem_cons.2 ⟨subset_closure ?_,
          Multiset.forall_mem_cons.2 ⟨subset_closure ?_, fun t ht => subset_closure (hs t ht)⟩⟩)
        · left; exact .of_mul_eq_one_right _ hk
        · left; exact ha₁
      · rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]
        left; exact hprod
    · rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, hc⟩
      · rw [hc]; rw [hc, mul_assoc] at hprod
        refine Submonoid.mul_mem _ (subset_closure ?_)
          (hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
        · right; exact ha₂
        rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
        exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
      rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod
      refine hind x c ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod)
      rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
      exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))

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]
ha : a ≠ 0
⊢ (a • p).roots = p.roots

Tactic:
by
  rw [smul_eq_C_mul, roots_C_mul _ ha]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - C a = 0
⊢ (C (1 - a)).degree ≤ ↑0

Tactic:
exact degree_C_le

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

Goal state before:
pp: case succ.refine_2
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
f : α →₀ ℕ
x✝ : f ∈ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
f_deg : degree f = n + 1
f_supp : ↑f.support ⊆ s
i : α
hi : i ∈ f.support
x : α →₀ ℕ
hx : f = x + single i 1
⊢ f ∈ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s

Tactic:
exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ content 0 = 0

Tactic:
by rw [← C_0, content_C, normalize_zero]

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

Goal state before:
pp: case neg.calc_2
α : 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
x : α
⊢ x ∈ Classical.choose ⋯ + Classical.choose ⋯ → Prime x

Tactic:
hadd

Goal state after:
case neg.calc_2
α : 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
x : α
hadd : x ∈ Classical.choose ⋯ + Classical.choose ⋯
⊢ Prime x
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
p q : R[X]
hpq : p * q = 0
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
mul_eq_zero

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
p q : R[X]
hpq : p = 0 ∨ q = 0
⊢ Associated (p * q).content (p.content * q.content)
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
⊢ count r s ≤ count r p.roots

Tactic:
rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
        Multiset.map_replicate fun a => X - C a, ← 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.Algebra.Polynomial.Roots

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

Tactic:
he

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
| ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).natDegree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.natDegree + q.natDegree = n
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
← p.natDegree_primPart,

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.natDegree + q.natDegree = n
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors = ⊤ ↔ a = 0

Tactic:
by
  nontriviality α
  exact ⟨fun h ↦ by rwa [← factors_prod a, FactorSet.prod_eq_zero_iff], fun h ↦ h ▸ factors_zero⟩

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

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ p.primPart.content ∣ 1

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (p.primPart.eraseLead * q.primPart).degree < ↑n

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n

Tactic:
content_primPart

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ 1 ∣ 1

R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (p.primPart.eraseLead * q.primPart).degree < ↑n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
⊢ a.factors ≤ b.factors ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, factors_mono⟩
  have : a.factors.prod ≤ b.factors.prod := prod_mono h
  rwa [factors_prod, factors_prod] at this

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ↑sa ≤ ↑sb
h_sb : b.factors = ↑sb
⊢ p.count ↑sa ≤ p.count ↑sb

Tactic:
count_some hp,

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ↑sa ≤ ↑sb
h_sb : b.factors = ↑sb
⊢ Multiset.count ⟨p, hp⟩ sa ≤ p.count ↑sb
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
⊢ ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s

Tactic:
by_contra! con

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
⊢ False