mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
p a b : α
nh : (∀ (n : ℕ), p ^ (n + 1) ∣ a) ∧ ∀ (n : ℕ), p ^ (n + 1) ∣ b
c : ℕ
hc : ¬p ^ (c + 1) ∣ a + b
⊢ False

Tactic:
simp_all [dvd_add]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: 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

Tactic:
minimalPeriod

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ (if h : 1 ∈ periodicPts fun x_1 ↦ x * x_1 then Nat.find h else 0) = 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.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
⊢ x ^ n = 1

Tactic:
by rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]

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

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
hp : Prime p
⊢ ¬p ^ (n.factorization p + 1) ∣ n

Tactic:
by
  intro h
  rw [← factorization_le_iff_dvd (pow_ne_zero _ hp.ne_zero) hn] at h
  simpa [hp.factorization] using h p

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * (b * a.minFac)
hb : a = b * a.minFac
⊢ a.minFac ∣ n

Tactic:
← mul_assoc

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * a.minFac
hb : a = b * a.minFac
⊢ a.minFac ∣ n
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
emultiplicity_eq_top,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ emultiplicity p b = ⊤
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)

Tactic:
simp only [Finset.sum_empty, Finset.prod_empty]

Goal state after:
case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p 1 = 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n.factorization p < n

pp: case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n

Tactic:
· exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
      Nat.lt_pow_self pp.one_lt

Goal state after:
case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n
Module: Mathlib.GroupTheory.OrderOfElement

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

pp: case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
· rw [h0, lcm_zero_left]
    apply dvd_zero

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * 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:
rw [orderOf, ← comp_mul_left]
  exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf 1 = 1

Tactic:
orderOf_one

Goal state after:
case pos
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ 1 = 1
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
⊢ ¬emultiplicity p (p * n)! = ⊤

Tactic:
emultiplicity_eq_top,

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
⊢ ¬¬FiniteMultiplicity p (p * n)!
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
h : IsOfFinOrder x
k : ℤ
h' : x ^ k ∈ zpowers x
⊢ IsOfFinOrder (x ^ k)

Tactic:
exact h.zpow

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k * (k ! * n !)) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)

Tactic:
← mul_assoc

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
Module: Mathlib.Data.Nat.Multiplicity

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

Tactic:
emultiplicity_choose hp hkn (lt_succ_self _),

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : 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})) + emultiplicity p k ≤ ↑n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_1
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p1

pp: case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2

Tactic:
· exact Nat.prime_of_mem_primeFactors p1.2

Goal state after:
case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
r : R
⊢ (expand R 1) (C r) = C r

Tactic:
rw [expand_C]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p %ₘ 0 = p

Tactic:
have := monic_zero_iff_subsingleton.mp h
    simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p /ₘ 0 = 0

Tactic:
have := monic_zero_iff_subsingleton.mp h
    simp [eq_iff_true_of_subsingleton]

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
a✝ : Nontrivial R
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
exact (degree_modByMonic_lt _ hq).le

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ -C ↑h.unit⁻¹ * (X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1

Tactic:
neg_mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C ↑h.unit⁻¹ * -(X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ q * p /ₘ q = p

Tactic:
refine (div_modByMonic_unique _ 0 hmo ⟨by rw [zero_add], ?_⟩).1

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ degree 0 < q.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
h : (C r).natDegree < (X - C a).natDegree
⊢ multiplicity (X - C a) (C r) = 0

Tactic:
multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
hp : derivative 0 = 0
⊢ natDegree 0 = 0

Tactic:
exact natDegree_zero

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

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ eval t (0 /ₘ (X - C t) ^ rootMultiplicity t 0) = (comp 0 (X + C t)).trailingCoeff

Tactic:
zero_divByMonic,

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ eval t 0 = (comp 0 (X + C t)).trailingCoeff
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i.down).sets

Tactic:
← iInf_sets_eq_finite,

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ i, f i).sets = (⨅ i, f i.down).sets
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case h
α : Type u
f : Filter α
hf : f.sets.Finite
⊢ f = 𝓟 (⋂₀ f.sets)

Tactic:
exact Filter.ext fun B ↦ ⟨sInter_subset_of_mem, mem_of_superset ((sInter_mem hf).2 (by simp))⟩

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:
rw [← not_iff_not]
  simp

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤

Tactic:
rintro ⟨b, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ (⇑derivative)^[n] ((X - C c) ^ n) = ↑n !

Tactic:
iterate_derivative_X_sub_pow,

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ n.descFactorial n • (X - C c) ^ (n - n) = ↑n !
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
⊢ TendstoCofinite _root_.id

Tactic:
simp [tendstoCofinite_iff_finite_preimage_singleton]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots.card ≤ p.natDegree

Tactic:
by
  by_cases hp0 : p = 0
  · simp [hp0]
  exact WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

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

Goal state before:
pp: case refine_2
α : 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
⊢ ∃ p_1, a ~ᵤ p_1 ∧ p ::ₘ s = {p_1}

Tactic:
use p

Goal state after:
case h
α : 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
⊢ a ~ᵤ p ∧ p ::ₘ s = {p}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case refine_1
σ : Type u_1
⊢ (Set.range fun a ↦ single a 1) ⊆ {d | degree d = 1}

pp: case refine_2
σ : Type u_1
⊢ {d | degree d = 1} ⊆ Set.range fun a ↦ single a 1

Tactic:
· simp [Set.range_subset_iff]

Goal state after:
case refine_2
σ : Type u_1
⊢ {d | degree d = 1} ⊆ Set.range fun a ↦ single a 1
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_5
s t : Set ℕ
n : ℕ
hn : n ∈ t
g : σ →₀ ℕ
hm : degree g ∈ s
f : σ →₀ ℕ
hgf : g ≤ g + f
e : degree g + n = degree (g + f)
⊢ g + f ∈ ⇑degree ⁻¹' s + ⇑degree ⁻¹' t

Tactic:
exact Set.add_mem_add hm (by simp_all)

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

Goal state before:
pp: case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
hc : c = 0
⊢ 0 ∈ q

Tactic:
← prod_eq_zero_iff,

Goal state after:
case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
hc : c = 0
⊢ q.prod = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
simp [h0]

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

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : r = 0
⊢ (C r * p).content = normalize r * p.content

Tactic:
simp [h0]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : r = 0
⊢ Associated (C r * p).content (r * p.content)

Tactic:
simp [h0]

Goal state after:
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
p : T[X]
ha : a ≠ 0
⊢ (C a * p).aroots S = p.aroots S

Tactic:
rw [aroots_def, Polynomial.map_mul, map_C, roots_C_mul]

Goal state after:
case ha
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
p : T[X]
ha : a ≠ 0
⊢ (algebraMap T S) a ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

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

Tactic:
by
  by_cases hp0 : p = 0
  · simp [hp0]
  refine ⟨fun h => ?_, Prime.irreducible⟩
  obtain ⟨f, hf⟩ := pf p hp0
  obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf
  rw [hq.prime_iff]
  exact hf.1 q (Multiset.mem_singleton_self _)

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

Goal state before:
pp: T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')

Tactic:
refine rootSet_maps_to' (fun h₀ => ?_) f

Goal state after:
T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S) p = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ IsUnit (C r).primPart

Tactic:
simp [h0]

Goal state after:
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
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0

Tactic:
iterate_derivative_X_sub_pow,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ eval t (m.choose b • (m.descFactorial (m - b) • (X - C t) ^ (m - (m - b)) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) =
    0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff

Tactic:
rw [gcd_comm (content _) _, gcd_comm (content _) _]
  apply gcd_content_eq_of_dvd_sub
  rw [← self_sub_C_mul_X_pow, ← self_sub_C_mul_X_pow, sub_mul, sub_sub, add_comm, sub_add,
    sub_sub_cancel, leadingCoeff_mul, map_mul, mul_assoc, mul_assoc]
  apply dvd_sub (Dvd.intro _ rfl) (Dvd.intro _ rfl)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ t.factors

Tactic:
rw [eq, factors_mul]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ s.factors + d.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ Quot.out (Associates.mk c ⊓ Associates.mk b)

Tactic:
rw [← mk_dvd_mk, Associates.quot_out, congr_fun₂ dvd_eq_le, le_inf_iff,
      mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ n * q.count p.factors = 0

Tactic:
count_eq_zero_of_ne hq hp h',

Goal state after:
case e'_4
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ n * 0 = 0
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: case neg
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Nontrivial M
α : S
hα : ⇑f = α • ⇑g
β : S
hβ : ⇑g = β • ⇑f
x : M
hx : x ≠ 0
⊢ ∃ α, f = α • g

Tactic:
have : (1 : S) • f x = (α * β) • f x := by simpa [hβ, smul_smul] using congr($hα x)

Goal state after:
case neg
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Nontrivial M
α : S
hα : ⇑f = α • ⇑g
β : S
hβ : ⇑g = β • ⇑f
x : M
hx : x ≠ 0
this : 1 • f x = (α * β) • f x
⊢ ∃ α, f = α • g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
p : R[X]
p_nonzero : p ≠ 0
hp : (aeval (r ^ n)) p = 0
⊢ (aeval r) ((expand R n) p) = 0

Tactic:
expand_aeval n p r

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
p : R[X]
p_nonzero : p ≠ 0
hp : (aeval (r ^ n)) p = 0
⊢ (aeval (r ^ n)) p = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ (↑x)⁻¹ = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)

Tactic:
inv_eq_of_root_of_coeff_zero_ne_zero this coeff_zero_ne,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ -((aeval ↑x) p.divX / (algebraMap K L) (p.coeff 0)) = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f i k hik) x) = z

Tactic:
by rw [of_f, hx]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : WellFoundedLT ι
inst✝¹ : SuccOrder ι
inst✝ : InverseSystem f
equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F i⁺), (e x).1 = f ⋯ x }
equivLim : (i : ι) → IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Iio i)), ↑(e x) l = f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ (globalEquiv equivSucc equivLim i) (f h x) = piLTProj h ((globalEquiv equivSucc equivLim j) x)

Tactic:
refine (DFunLike.congr_fun ?_ _).trans ((globalEquivAux equivSucc equivLim j).nat le_rfl h h x)

Goal state after:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : WellFoundedLT ι
inst✝¹ : SuccOrder ι
inst✝ : InverseSystem f
equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F i⁺), (e x).1 = f ⋯ x }
equivLim : (i : ι) → IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Iio i)), ↑(e x) l = f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ globalEquiv equivSucc equivLim i = (globalEquivAux equivSucc equivLim j).equiv ⟨i, h⟩
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ restrictSupport R 0 = 1

Tactic:
apply le_antisymm
  · rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
    simp only [monomial, AddMonoidAlgebra.lsingle_apply, zero_subset, mem_preimage,
      ← AddMonoidAlgebra.one_def, SetLike.mem_coe, Submodule.mem_one, algebraMap_eq]
    exact ⟨1, by simp⟩
  · rintro _ ⟨x, rfl⟩
    simp [mem_restrictSupport_iff, subset_def, coeff, AddMonoidAlgebra.one_def,
      Finsupp.single_apply]

Goal state after: