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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
p✝ : R[X]
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ map f 0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
i : ℕ
⊢ (derivativeFinsupp (map f p)) i = (Finsupp.mapRange (fun x ↦ map f x) ⋯ (derivativeFinsupp p)) i

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (derivativeFinsupp (derivative p)) i = (Finsupp.comapDomain Nat.succ (derivativeFinsupp p) ⋯) i

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) =
    0 + (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p)

Tactic:
simp

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

Goal state before:
pp: case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0

Tactic:
· exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))

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

Goal state before:
pp: case empty
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
⊢ ⋂ i ∈ ∅, s i ∈ f ↔ ∀ i ∈ ∅, s i ∈ f

Tactic:
simp

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : p.IsRoot a
⊢ p = (X - C a) * (p /ₘ (X - C a))

Tactic:
mul_divByMonic_eq_iff_isRoot.2 h

Goal state after:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : p.IsRoot a
⊢ p = p
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.right
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
apply le_antisymm <;> rw [le_iInf_iff] <;> intro i

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

case a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ derivative (p ^ (Nat.zero + 1)) = C (↑Nat.zero + 1) * p ^ Nat.zero * derivative p

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ derivative (p ^ Nat.zero) = C ↑Nat.zero * p ^ (Nat.zero - 1) * derivative p

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ 𝓟 ⊤ ≤ f ↔ f = ⊤

Tactic:
simp

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

Goal state before:
pp: case neg.h₁
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)

Tactic:
apply dvd_mul_of_dvd_right

Goal state after:
case neg.h₁
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ - p₂ %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case h₂
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ * (p₁ - p₁ %ₘ q)

Tactic:
apply dvd_mul_of_dvd_right

Goal state after:
case h₂
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ - p₁ %ₘ q
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 ↑n * eval c ((⇑derivative)^[m] (f ^ (n - 1) * derivative f))

Tactic:
eval_natCast

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ ↑n * eval c ((⇑derivative)^[m] (f ^ (n - 1) * derivative f))
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.succ] (f ^ n))

Tactic:
rw [Function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_natCast,
    iterate_derivative_natCast_mul, eval_mul, eval_natCast]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
⊢ (⇑derivative)^[0] ((X + C c) ^ n) = n.descFactorial 0 • (X + C c) ^ (n - 0)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
⊢ ∀ a ∈ range n.succ,
    a ∈ range (min m n).succ →
      (n.choose a * m.descFactorial a) • ((⇑derivative)^[n - a] p * X ^ (m - a)) =
        (n.choose a * m.descFactorial a) • ((⇑derivative)^[n - a] p * X ^ (m - a))

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
t : Set ((i : ι) → α i)
⊢ (∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, True) ∧ (i.1.pi fun i ↦ s i) ⊆ t) ↔ ∃ I, I.Finite ∧ I.pi s ⊆ t

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u
ι : Type w
f : ι → Set α
⊢ ⨅ i ∈ ∅, 𝓟 (f i) = 𝓟 (⋂ i ∈ ∅, f i)

Tactic:
simp

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

Goal state before:
pp: case e'_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ X = X ^ 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
f : Filter α
hf : f.sets.Finite
B : Set α
⊢ ∀ U ∈ f.sets, U ∈ f

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Finite α
f : Filter α
⊢ f.sets ⊆ 𝒫 univ

Tactic:
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:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n] (derivative p * X) = (⇑derivative)^[n + 1] p * X + n • (⇑derivative)^[n] p

Tactic:
convert! (derivative p).iterate_derivative_mul_X_pow n 1

Goal state after:
case e'_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ X = X ^ 1

case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n + 1] p * X + n • (⇑derivative)^[n] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) • ((⇑derivative)^[n - k] (derivative p) * X ^ (1 - k))
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
⊢ pi f₁ = pi f₂ ↔ f₁ = f₂

Tactic:
refine ⟨fun h => ?_, congr_arg pi⟩
  have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
  have : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
  exact hle.antisymm (pi_le_pi.1 h.ge)

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
⊢ ∂ ⊤ = ⊥

Tactic:
by rw [boundary, hnot_top, inf_bot_eq]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ derivative (eval₂ C q (C r)) = eval₂ C q (derivative (C r)) * derivative q

Tactic:
eval₂_C,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ derivative (C r) = eval₂ C q (derivative (C r)) * derivative q
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

Tactic:
map_swap4_eq_comap,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set M
⊢ ⇑ofAdd '' (0 • s) = (⇑ofAdd '' s) ^ 0

Tactic:
simp

Goal state after:
case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set M
⊢ {1} = 1
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set (Multiplicative M)
⊢ ⇑toAdd '' s ^ 0 = 0 • ⇑toAdd '' s

Tactic:
simp

Goal state after:
case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set (Multiplicative M)
⊢ {0} = 0
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i)

Tactic:
by
  refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_
  refine ((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_
  rintro ⟨I, s⟩ ⟨hI : I.Finite, hs : ∀ i ∈ I, s i ∈ l i⟩
  classical
  rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]
  refine univ_pi_mem_pi (fun i ↦ ?_) ?_
  · by_cases hi : i ∈ I
    · simpa [hi] using image_mem_map (hs i hi)
    · simp [hi]
  · filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)
    simp [hiI, hsurj.range_eq]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
inst✝ : Finite ι
f : (i : ι) → α i → β i
l : (i : ι) → Filter (α i)
⊢ ∀ᶠ (i : ι) in cofinite, Surjective (f i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
⊢ pure a ×ˢ pure b = pure (a, b)

Tactic:
simp

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s : Multiset ι
f : ι → R[X]
⊢ derivative (Multiset.map f 0).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (Multiset.erase 0 i)).prod * derivative (f i)) 0).sum

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : α → β
a : α
b : β
⊢ cofinite ≤ 𝓟 {a}ᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
f : Filter α
x : α
h : {x}ᶜ ∈ f
⊢ x ∉ {x}ᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ⊥.coprod ⊥ = ⊥

Tactic:
simp

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 : ι
a'' : α
i'' : ι
left✝ : (a'', i'') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
⊢ ((fun x ↦ b) a'', id i'') ∈ {b} ×ˢ univ

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
f : R[X]
⊢ derivative (↑n * f) = ↑n * derivative f

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ (⇑derivative)^[0] (p.comp (1 - X)) = (-1) ^ 0 * ((⇑derivative)^[0] p).comp (1 - X)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hk : 0 ≤ #S
⊢ (⇑derivative)^[0] (∏ a ∈ S, (X - C a)) = ↑0! * ∑ T ∈ powersetCard (#S - 0) S, ∏ a ∈ T, (X - C a)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
b : β
⊢ {b}.Finite

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
f : α → β
g : β → ι
inst✝¹ : TendstoCofinite g
inst✝ : TendstoCofinite f
r : ι
⊢ {b | b = r}.Finite

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
⊢ (∀ x ∈ p ::ₘ f, Prime x) → (∀ x ∈ g, Prime x) → (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g

Tactic:
hf

Goal state after:
case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
⊢ (∀ x ∈ g, Prime x) → (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ p ∈ p ::ₘ f

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ p ∣ (p ::ₘ f).prod

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset M
⊢ (Multiset.map Associates.mk 0).prod = Associates.mk (Multiset.prod 0)

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset (Associates M)
⊢ Multiset.prod 0 = 1 ↔ ∀ a ∈ 0, a = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p ∈ p ::ₘ f

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) 0, Prime x

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ roots 0 = 0 ↔ 0 = 0 ∨ IsRoot 0 = ⊥

Tactic:
simp

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

Goal state before:
pp: case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ w s ≤ (weight w) f

Tactic:
exact le_weight_of_ne_zero' w hs

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) 0, normalize x = x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
this : Multiset.Rel Associated (p ::ₘ normalizedFactors b) (normalizedFactors a)
⊢ p ∈ p ::ₘ normalizedFactors b

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
R✝ : Type u_3
inst✝¹ : Semiring R✝
w : σ → M
R : Type u_4
inst✝ : AddCommMonoid R
⊢ ∑ i ∈ support 0, 0 i = 0

Tactic:
simp

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

Goal state before:
pp: case h
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ f.support ⊆ Finset.univ

Tactic:
simp

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

Goal state before:
pp: case hf
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∀ x ∈ Finset.univ, x ∉ f.support → f x = 0

Tactic:
simp

Goal state after:
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
⊢ ↑u * (p ::ₘ s).prod = ↑u * (p * s.prod)

Tactic:
simp

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

Goal state before:
pp: σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
i : σ
hi : i ∈ f.support
⊢ single i 1 ≤ f

Tactic:
simp

Goal state after:
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
i : σ
hi : i ∈ f.support
⊢ 1 ≤ f i
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
i : σ
hi : i ∈ f.support
⊢ degree (g + single i 1) = degree g + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ (p ::ₘ fx).prod ~ᵤ a * b

Tactic:
rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _

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
this : Rel Associated (p ::ₘ factors b) (factors a)
⊢ p ∈ p ::ₘ factors b

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (ofMultiset s).roots = s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
⊢ p ∣ a

Tactic:
by_cases hcases : a = 0

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ a

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : ¬a = 0
⊢ p ∣ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
h : 0 ~ᵤ 0
⊢ Rel Associated (factors 0) (factors 0)

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
h✝ : Subsingleton α
h : ∀ p ∈ 0, Prime p
⊢ normalizedFactors (Multiset.prod 0) = 0

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hx : IsUnit 0
⊢ normalizedFactors 0 = 0

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Subsingleton α
hs : 0 ∉ 0
⊢ normalizedFactors (Multiset.prod 0) = (Multiset.map normalizedFactors 0).sum

Tactic:
simp

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

Goal state before:
pp: case inr.empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
hs : 0 ∉ 0
⊢ normalizedFactors (Multiset.prod 0) = (Multiset.map normalizedFactors 0).sum

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ 0 < 2

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
x : α
⊢ x ∈ normalizedFactors 0 ↔ ↑f x ∈ normalizedFactors (f 0)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (if 1 = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors 1)).prod) = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s✝ : Set α
s : Set (α →₀ ℕ)
⊢ ((fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) ∘ ⇑Multiplicative.toAdd) 1 = 1

Tactic:
simp

Goal state after: