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

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
orderOf,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ minimalPeriod (fun x_1 ↦ x * x_1) 1 = n ↔
    IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1
Module: Mathlib.Data.Nat.Factorization.Defs

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

pp: case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization

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

Goal state after:
case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
⊢ orderOf 1 = 1

Tactic:
orderOf,

Goal state after:
G : Type u_1
inst✝ : Monoid G
⊢ minimalPeriod (fun x ↦ 1 * x) 1 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 1 ↔ x = 1

Tactic:
orderOf,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ minimalPeriod (fun x_1 ↦ x * x_1) 1 = 1 ↔ x = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ Set.InjOn (fun x_1 ↦ x ^ x_1) (Set.Iio (orderOf x))

Tactic:
by
  simpa only [mul_left_iterate_apply_one]
    using! iterate_injOn_Iio_minimalPeriod (f := (x * ·)) (x := 1)

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

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
← factorization_le_iff_dvd hd hn

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList

Tactic:
List.subperm_ext_iff

Goal state after:
n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
hfin.emultiplicity_eq_multiplicity,

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ ↑(multiplicity p (a * b)) = emultiplicity p a + emultiplicity p b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0

Tactic:
· contrapose hr0
    exact (add_eq_zero.1 hr0).2

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n

Tactic:
← factorization_le_iff_dvd hd hn

Goal state after:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d.factorization ≤ n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ n.factorization p

Tactic:
pp.pow_dvd_iff_le_factorization hn

Goal state after:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ k ≤ n.factorization p ↔ k ≤ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: d n : ℕ
h : d ∣ n
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Goal state after:
case inl
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
if pp : p.Prime then ?_ else
    simp [pp]

Goal state after:
n p : ℕ
hn : ¬n = 0
pp : Prime p
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ orderOf (x * y) ∣ (orderOf x).lcm (orderOf y)

Tactic:
orderOf,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod (fun x_1 ↦ x * y * x_1) 1 ∣ (orderOf x).lcm (orderOf y)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ orderOf (x * y) = orderOf x * orderOf y

Tactic:
orderOf,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod (fun x_1 ↦ x * y * x_1) 1 = orderOf x * orderOf y
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1

Tactic:
orderOf,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod (fun x_1 ↦ x * x_1) 1 = p ↔ x ^ p = 1 ∧ x ≠ 1
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Goal state after:
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n

case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp

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

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
intro n c c0
    rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]
    split_ifs with n0
    · simp [n0]
    · exact natDegree_C_mul_X_pow (n - 1) c c0

Goal state after:
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
h' : C (p.coeff 0) ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
eq_C_of_degree_le_zero h,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ (C (p.coeff 0)).divX.degree < ((C (p.coeff 0)).divX * X + C ((C (p.coeff 0)).coeff 0)).degree
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : a ≤ g • a
⊢ g • a = a

Tactic:
exact le_antisymm h key

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (p + C a).degree
h : p.degree ≤ 0
⊢ 0 < (C a).degree

Tactic:
eq_C_of_degree_le_zero h,

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (C (p.coeff 0) + C a).degree
h : p.degree ≤ 0
⊢ 0 < (C a).degree
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o

Tactic:
exact Iff.mp ne_comm h

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
⊢ (p ^ m).coeff o = if o = m * n then a ^ m else 0

Tactic:
by
  split_ifs with h
  · subst h h_pow_bas
    exact coeff_pow_of_natDegree_le ‹_›
  · apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)
    · exact natDegree_pow_le_of_le m ‹_›
    · exact Iff.mp ne_comm h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).leadingCoeff = f.leadingCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).coeff ((expand R p) f).natDegree = f.coeff f.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case add
R : Type u
inst✝ : Semiring R
g p✝ q✝ : R[X]
a✝¹ : derivative (p✝ * g) = derivative p✝ * g + p✝ * derivative g
a✝ : derivative (q✝ * g) = derivative q✝ * g + q✝ * derivative g
⊢ derivative ((p✝ + q✝) * g) = derivative (p✝ + q✝) * g + (p✝ + q✝) * derivative g

Tactic:
simp only [add_mul, map_add, add_assoc, add_left_comm, *]

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
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p %ₘ q = q * (r - p /ₘ q)

Tactic:
modByMonic_eq_sub_mul_div,

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
hpq0 : ¬p %ₘ q = 0
⊢ p - q * (p /ₘ q) = q * (r - p /ₘ q)
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)).leadingCoeff = 0

Tactic:
leadingCoeff,

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a (p %ₘ (X - C a)) = eval a p

Tactic:
modByMonic_eq_sub_mul_div,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a (p - (X - C a) * (p /ₘ (X - C a))) = eval a p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p

Tactic:
modByMonic_eq_sub_mul_div,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
p : ι' → Prop
s✝ : ι' → Set α
s : Set (Set α)
hsc : s.Countable
hs : (generate s).HasBasis p s✝
⊢ ∃ x, generate s = ⨅ i, 𝓟 (x i)

Tactic:
rw [generate_eq_biInf]

Goal state after:
α : Type u_1
ι' : Sort u_5
p : ι' → Prop
s✝ : ι' → Set α
s : Set (Set α)
hsc : s.Countable
hs : (generate s).HasBasis p s✝
⊢ ∃ x, ⨅ s_1 ∈ s, 𝓟 s_1 = ⨅ i, 𝓟 (x i)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i ↦ s (x i)

Tactic:
obtain ⟨x', hx'⟩ : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i) := by
    rcases h with ⟨s, hsc, rfl⟩
    rw [generate_eq_biInf]
    exact countable_biInf_principal_eq_seq_iInf hsc

Goal state after:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i ↦ s (x i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree

Tactic:
leadingCoeff,

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).coeff (derivative p).natDegree = p.leadingCoeff * ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).coeff (derivative p).natDegree = p.leadingCoeff * ↑p.natDegree

Tactic:
leadingCoeff,

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).coeff (derivative p).natDegree = p.coeff p.natDegree * ↑p.natDegree
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Tactic:
constructor
  · rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
    exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
  · rintro ⟨t₁, ht₁, t₂, ht₂, h⟩
    exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p * u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u

Tactic:
rw [mul_ne_zero_iff] at hq

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
c : R
m : ℕ
⊢ C ↑m * (X - C c) ^ (m - 1) * derivative (X - C c) = C ↑m * (X - C c) ^ (m - 1)

Tactic:
derivative_X_sub_C,

Goal state after:
R : Type u
inst✝ : CommRing R
c : R
m : ℕ
⊢ C ↑m * (X - C c) ^ (m - 1) * 1 = C ↑m * (X - C c) ^ (m - 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
c : R
⊢ C 2 * (X - C c) * derivative (X - C c) = C 2 * (X - C c)

Tactic:
derivative_X_sub_C,

Goal state after:
R : Type u
inst✝ : CommRing R
c : R
⊢ C 2 * (X - C c) * 1 = C 2 * (X - C c)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
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
h✝ : ¬derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
case neg hP' =>
        have hP'' : P.natDegree ≠ 0 := by
          contrapose hP'
          exact derivative_of_natDegree_zero hP'
        refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_
        linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']

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

Goal state before:
pp: case a
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
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ ∑ a ∈ T, (∏ a ∈ T.erase a, (X - C a)) * derivative (X - C a) = ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)

Tactic:
derivative_X_sub_C,

Goal state after:
case a
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
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ ∑ x ∈ T, (∏ a ∈ T.erase x, (X - C a)) * 1 = ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl.refine_2
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 * y)
hc : x = c✝ * c
⊢ s.prod ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))

Goal state after:
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✝ * (x * c)
hc : y = c✝ * c
⊢ s.prod ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
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
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑p.roots.card ≤ p.degree

Tactic:
by
  classical
  unfold roots
  rw [dif_neg hp0]
  exact (Classical.choose_spec (exists_multiset_roots hp0)).1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ (p ::ₘ factors b).prod

Tactic:
by
            rw [prod_cons]; exact (factors_prod hb0).symm.mul_left _

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ α → ℕ∞

pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∀ {a b : α}, DvdNotUnit a b → ?refine_1 a < ?refine_1 b

Tactic:
· intro a
      by_cases h : a = 0
      · exact ⊤
      exact ↑(Multiset.card (Classical.choose (pf a h)))

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∀ {a b : α},
    DvdNotUnit a b →
      (if h : a = 0 then ⊤ else ↑(Classical.choose ⋯).card) < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card
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]
⊢ (-map (algebraMap T S) p).roots = p.aroots S

Tactic:
roots_neg

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: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.leadingCoeff = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
leadingCoeff,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.coeff p.natDegree = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content
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
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) = gcd p.leadingCoeff p.eraseLead.content

Tactic:
leadingCoeff,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) = gcd (p.coeff p.natDegree) p.eraseLead.content
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
nontriviality S
  rw [eq_C_content_mul_primPart p, map_mul, aeval_C] at hp
  refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp
  have : IsDomain R := { Module.nontrivial R S with }
  rwa [(FaithfulSMul.algebraMap_injective R S).ne_iff' (map_zero _), Ne, content_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ x ∈ Finset.image (fun s ↦ ↑s.2 * s.1.prod) ((normalizedFactors y).powerset.toFinset ×ˢ Finset.univ) ↔ x ∣ y

Tactic:
simp only [Finset.mem_image, Finset.mem_product, Finset.mem_univ, and_true,
    Multiset.mem_toFinset, Multiset.mem_powerset]

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ (∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x) ↔ x ∣ y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False

Tactic:
exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Multiset.map (fun a ↦ ↑a) (factors' a) = Multiset.map (fun a ↦ ↑a) (factors' b)

Tactic:
map_subtype_coe_factors',

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Multiset.map Associates.mk (factors a) = Multiset.map (fun a ↦ ↑a) (factors' b)