mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
h₅ : q - f /ₘ g = 0
⊢ r - f %ₘ g = 0

Tactic:
simpa [h₅] using h₁

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k : ℕ
p : R[X]
m : ℕ
⊢ ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)

Tactic:
by
  induction k generalizing m with
  | zero => simp
  | succ k ih =>
      calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]

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

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

Tactic:
mul_assoc,

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

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

Tactic:
rw [modByMonic_eq_zero_iff_dvd hq]
  exact dvd_mul_right q p

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
| p

Tactic:
rw [← modByMonic_add_div p 1]; simp

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
| p /ₘ 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (C ↑n * f ^ (n - 1) * derivative f))

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (C ↑n * (f ^ (n - 1) * derivative f)))
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
Ifin : I.Finite
V : ↑I → Set α
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i ∈ ⨅ i, s i

Tactic:
exact mem_iInf_of_iInter Ifin V_in Subset.rfl

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

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (p.comp (X + C t)).trailingCoeff

Tactic:
rw [← congr_arg (comp · <| X + C t) mul_eq, mul_comp, pow_comp, sub_comp, X_comp, C_comp,
    add_sub_cancel_right, ← reverse_leadingCoeff, reverse_X_pow_mul, reverse_leadingCoeff,
    trailingCoeff, Nat.le_zero.1 (natTrailingDegree_le_of_ne_zero <|
      this ▸ eval_divByMonic_pow_rootMultiplicity_ne_zero t hp), this]

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
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ (pi f).HasBasis (fun Ik ↦ Ik.1.Finite ∧ p Ik.2) fun Ik ↦ Ik.1.pi fun i ↦ s i Ik.2

Tactic:
by
  refine hasBasis_pi h |>.to_hasBasis ?_ ?_
  · rintro ⟨I, k⟩ ⟨hI, hk⟩
    rcases h_dir I k hI hk with ⟨k₀, hk₀, hk₀'⟩
    exact ⟨⟨I, k₀⟩, ⟨hI, hk₀⟩, Set.pi_mono hk₀'⟩
  · rintro ⟨I, k⟩ ⟨hI, hk⟩
    exact ⟨⟨I, fun _ ↦ k⟩, ⟨hI, fun _ _ ↦ hk⟩, subset_rfl⟩

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

Goal state before:
pp: α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x

Tactic:
by
  simpa only [Filter.Eventually, ofPred_forall] using iInter_mem

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

Goal state before:
pp: ⊢ cofinite = atTop

Tactic:
refine le_antisymm ?_ atTop_le_cofinite
  refine atTop_basis.ge_iff.2 fun N _ => ?_
  simpa only [mem_cofinite, compl_Ici] using! finite_lt_nat N

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

Goal state before:
pp: case mp
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ

pp: case mpr
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ

Tactic:
· rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
    simp

Goal state after:
case mpr
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
Module: Mathlib.Algebra.BigOperators.Associated

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

Tactic:
mul_assoc,

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

Tactic:
weight_apply

Goal state after:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
| (f - single i 1 + single i 1).sum fun i c ↦ c • w i
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 = ((f - single i 1).sum fun i c ↦ c • w i) + w i

pp: σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ 0 • w i = 0

pp: case h_zero
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ), 0 • w a = 0

pp: case h_add
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a

Tactic:
weight_apply

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

σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ 0 • w i = 0

case h_zero
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ), 0 • w a = 0

case h_add
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * q * (s.erase q).prod

Tactic:
mul_assoc,

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * (q * (s.erase q).prod)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝ : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
hx : x ∈ normalizedFactors x✝ + normalizedFactors y
⊢ Irreducible x

Tactic:
rcases Multiset.mem_add.1 hx with (hx | hx) <;> exact irreducible_of_normalized_factor x hx

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
ha : a ≠ 0
n : ℕ
⊢ ((monomial n) a).roots = n • {0}

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
ha : a ≠ 0
n : ℕ
⊢ (C a * X ^ n).roots = n • {0}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : 0 < n
a x : R
⊢ x ∈ nthRoots n a ↔ x ^ n = a

Tactic:
mem_nthRoots h

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : 0 < n
a x : R
⊢ x ^ n = a ↔ x ^ n = a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ ((monomial k) r).content = normalize r

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ (C r * X ^ k).content = normalize r
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ ((monomial n) a).aroots S = n • {0}

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ (C a * X ^ n).aroots S = n • {0}
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
h : p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

pp: case neg
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
h : ¬p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
· simp only [h, map_zero, rootMultiplicity_zero]

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
h : ¬p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1
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:
eraseLead_coeff,

Goal state after:
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 = if i = p.natDegree then 0 else p.coeff i
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬(X - C t) ^ (m - 1) * (X - C t) ∣ (X - C t) ^ (m - 1) * C ↑m * g

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬(X - C t) ^ (m - 1) * (X - C t) ∣ (X - C t) ^ (m - 1) * (C ↑m * g)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
⊢ a ∣ b * c → a ∣ c

Tactic:
by
  simpa [mul_comm b c] using dvd_of_dvd_mul_left_of_no_prime_factors ha @no_factors

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart.natDegree = p.natDegree

Tactic:
by
  nontriviality R
  by_cases h : C p.content = 0
  · rw [C_eq_zero, content_eq_zero_iff] at h
    simp [h]
  conv_rhs =>
    rw [p.eq_C_content_mul_primPart, natDegree_mul h p.primPart_ne_zero, natDegree_C, zero_add]

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

Goal state before:
pp: case pos.refine_1
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 a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * a' = p * a

Tactic:
mul_assoc,

Goal state after:
case pos.refine_1
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 a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * (c' * a') = p * a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart

Tactic:
rw [← normalize_eq_zero, ← C_eq_zero] at h0

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos.refine_2
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 a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * b' = p * b

Tactic:
mul_assoc,

Goal state after:
case pos.refine_2
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 a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * (c' * b') = p * b
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ C r * C ↑(normUnit r) * C ↑(normUnit r)⁻¹ = C r

Tactic:
mul_assoc,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ C r * (C ↑(normUnit r) * C ↑(normUnit r)⁻¹) = C r
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
⊢ eval t (m.choose 0 • ((⇑derivative)^[m - 0] ((X - C t) ^ m) * (⇑derivative)^[0] (p /ₘ (X - C t) ^ m))) =
    m ! • eval t (p /ₘ (X - C t) ^ m)

Tactic:
rw [m.choose_zero_right, one_smul, eval_mul, m.sub_zero, iterate_derivative_X_sub_pow_self,
      eval_natCast, nsmul_eq_mul]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * X ^ p.natDegree * q - C p.leadingCoeff * C q.leadingCoeff * X ^ (p * q).natDegree

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * C q.leadingCoeff * X ^ (p * q).natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ ↑(a ⊔ b) + ↑a ⊓ ↑b = ↑a + ↑b

Tactic:
← WithTop.coe_inf,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ ↑(a ⊔ b) + ↑(a ⊓ b) = ↑a + ↑b
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (C p.content * p.primPart * (C q.content * q.primPart)).content
    ((C p.content * p.primPart).content * (C q.content * q.primPart).content)

Tactic:
mul_assoc,

Goal state after:
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (C p.content * (p.primPart * (C q.content * q.primPart))).content
    ((C p.content * p.primPart).content * (C q.content * q.primPart).content)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (C q.content * q.primPart * p.primPart).content)
    (p.content * p.primPart.content * (C q.content * q.primPart).content)

Tactic:
mul_assoc,

Goal state after:
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (C q.content * (q.primPart * p.primPart)).content)
    (p.content * p.primPart.content * (C q.content * q.primPart).content)
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
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : Nat.find h ≤ s.natDegree
⊢ False

Tactic:
← rdeg

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
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = C a * p * (C a⁻¹ * r)

Tactic:
mul_assoc,

Goal state after:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = C a * (p * (C a⁻¹ * r))
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = C a * p * (C a⁻¹ * r)

Tactic:
rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp : p ≠ 0
⊢ ↑(normUnit p) = C p.leadingCoeff⁻¹

Tactic:
by
  have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp
  simp [CommGroupWithZero.coe_normUnit _ this]

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)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a

Tactic:
rw [← Associates.mk_le_mk_iff_dvd]
  refine
    ⟨fun h =>
      Associates.le_of_count_ne_zero (Associates.mk_ne_zero.mpr ha0)
        (Associates.irreducible_mk.mpr hp) h,
      fun h => ?_⟩
  rw [← pow_one (Associates.mk p),
    Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr ha0)
      (Associates.irreducible_mk.mpr hp)] at h
  exact (zero_lt_one.trans_le h).ne'

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]

Goal state after:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ (∀ (q : R[X]), q.degree ≤ ↑((p * C p.leadingCoeff⁻¹).natDegree / 2) → q ∣ p * C p.leadingCoeff⁻¹ → IsUnit q) ↔
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ p * C p.leadingCoeff⁻¹ ≠ 1