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

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x ^ orderOf x = 1

Tactic:
pow_orderOf_eq_one

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ 1 = 1
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
by
  constructor
  · intro h
    by_cases n_zero : n = 0
    · simp [n_zero]
    · right
      rw [← h]
      exact not_dvd_ordCompl hp n_zero
  · 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.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ ((p ^ n).choose k).factorization p + k.factorization p ≤ n

Tactic:
factorization_choose hp hkn (lt_succ_self _),

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) + k.factorization p ≤ n
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
rw [factorization_choose hp hkn (Nat.lt_add_one _)]

Goal state after:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ #({i ∈ Ico 1 (log p n + 1) | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) ≤ log p n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ k, orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
⊢ x ^ orderOf x = 1

Tactic:
pow_orderOf_eq_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ k, orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
⊢ 1 = 1
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
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Tactic:
mul_sum

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1

Tactic:
hp.emultiplicity_self,

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ x ^ orderOf x = 1

pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ 1 ≤ orderOf x

Tactic:
pow_orderOf_eq_one

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ 1 = 1

G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ 1 ≤ orderOf x
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑n - ↑(multiplicity p k)

Tactic:
rw [← emultiplicity_choose_prime_pow_add_emultiplicity hp hkn hk0,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, Nat.pos_of_ne_zero hk0⟩).emultiplicity_eq_multiplicity,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, choose_pos hkn⟩).emultiplicity_eq_multiplicity]

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑(multiplicity p ((p ^ n).choose k)) =
    ↑(multiplicity p ((p ^ n).choose k)) + ↑(multiplicity p k) - ↑(multiplicity p k)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : emultiplicity p k = ↑n
⊢ p ^ n ∣ k

Tactic:
emultiplicity_eq_coe

Goal state after:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
use c

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := ⋯
c : ℕ := ⋯
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
⊢ a = c ^ n ∧ b = c ^ m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: 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) = 0
⊢ Nonempty R

Tactic:
exact ⟨0⟩

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

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
| a ^ m

Tactic:
rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]

Goal state after:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
| a ^ (m' * g)
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
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
exact natDegree_pow_le_of_le m ‹_›

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

Goal state before:
pp: case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
· intro hn
      rw [notMem_support_iff.1 hn]
      split_ifs <;> rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Prime X

Tactic:
by
  convert! prime_X_sub_C (0 : R)
  simp

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

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

Tactic:
obtain ⟨u, -, h⟩ := isUnit_iff.mp h
    apply not_le.mpr (zero_lt_one' (WithBot ℕ))
    simp [← hp, ← h, degree_C_le]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
have := natDegree_derivative_lt hp

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
this : (derivative p).natDegree < p.natDegree
⊢ (⇑derivative)^[t] (derivative p) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0
      rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
        degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
      exact
        Nat.cast_lt.2
          (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
            by simpa [degree_eq_natDegree hq.ne_zero] using! h0q))

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = 0

Tactic:
by simp only [h0, natDegree_zero]

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
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ (p %ₘ q).leadingCoeff = 0

Tactic:
by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero]

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

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

Tactic:
smul_C,

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

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i

Tactic:
mul_sum

Goal state after:
case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mpr
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
· rcases h with ⟨t, hts, tfin, h⟩
    exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ i, V i

Tactic:
simp only [mem_iInf, biInter_eq_iInter]

Goal state after:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) ↔
    ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ x, V ↑x ∧ U = ⋂ i, V i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Tactic:
nontriviality
  have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
    simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
      Nat.WithBot.one_le_iff_zero_lt] using hdegree
  nth_rw 2 [← modByMonic_add_div p q]
  rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]
  rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]
  exact (degree_modByMonic_lt p hmonic).trans_le hdegree

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

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

Tactic:
suffices ((n + 1 + 1) * (n + 1) / 2) * 2 = (n + 1 + 1) * (n + 1) by
    simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]
    ring

Goal state after:
case succ.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h

Tactic:
← comap_equiv_symm,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ).symm) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
hnot_boundary,

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢∂ a \ ￢a = ￢￢a

Tactic:
hnot_boundary,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ \ ￢a = ￢￢a
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
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
j : ι
hj : j ∈ s
hij : ¬i = j
⊢ (Multiset.map f (i ::ₘ s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)

Tactic:
simp [hij]

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

Goal state before:
pp: case refine_4.refine_2
α : 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
hqk : f.ker = q.1
⊢ Disjoint (𝓟 f.ker) q.2

Tactic:
hqk

Goal state after:
case refine_4.refine_2
α : 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
hqk : f.ker = q.1
⊢ Disjoint (𝓟 q.1) q.2
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_3
α : 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
hqk : f.ker = q.1
⊢ ⊥ ⊔ Coheyting.boundary q.2 ≤ q.2

Tactic:
bot_sup_eq

Goal state after:
case refine_4.refine_3
α : 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
hqk : f.ker = q.1
⊢ Coheyting.boundary q.2 ≤ q.2
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

Goal state after:
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}
hprod : (c ::ₘ s).prod = x * y
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
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
⊢ ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) =
    (↑k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
mul_sum

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
⊢ ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) =
    ∑ i ∈ powersetCard (#S - (k + 1)) S, (↑k + 1) * ∏ a ∈ i, (X - C a)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a

Tactic:
· exact normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q

Tactic:
convert!
    normalize_eq_normalize hdvd
      ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
        (prime_of_normalized_factor _ hq).irreducible hdvd) <;>
    apply (normalize_normalized_factor _ ‹_›).symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
· rw [pow_succ', succ_nsmul']
      refine Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_
      refine Rel.add ?_ <| factors_pow n
      exact rel_refl_of_refl_on fun y _ => Associated.refl _

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
x : α
hx : x ≠ 0
⊢ (∑ a ∈ (factors x).toFinset, count a (factors x) • {a}).prod = (factors x).prod

Tactic:
toFinset_sum_count_nsmul_eq (factors x)

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
x : α
hx : x ≠ 0
⊢ (factors x).prod = (factors x).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < normalizedFactors x

Tactic:
obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h

Goal state after:
case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ 0 < normalizedFactors x
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.content = 0
⊢ Associated p.content (p.content * p.primPart.content)

Tactic:
conv_lhs => rw [p.eq_C_content_mul_primPart]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ Associated (C p.content * p.primPart).content (p.content * p.primPart.content)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < (q * C q.leadingCoeff⁻¹).degree

Tactic:
exact degree_modByMonic_lt p (monic_mul_leadingCoeff_inv hq)

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact normalize_associated (a * b)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ ((monomial n) a).rootSet S = {0}

Tactic:
by
  classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

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

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
ha0 : p.count a.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count b.factors

Tactic:
ha0,

Goal state after:
case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
ha0 : p.count a.factors = 0
⊢ 0 + p.count b.factors = p.count b.factors
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
⊢ (gcd p q).degree ≤ p.degree

Tactic:
have := natDegree_le_iff_degree_le.mp (natDegree_le_of_dvd (gcd_dvd_left p q) hp)
  rwa [degree_eq_natDegree hp]

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

Goal state before:
pp: F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
⊢ 0 < f.natDegree

Tactic:
exact h.natDegree_pos

Goal state after: