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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Semiring S
p : S[X]
f : S →+* R
hf : Function.Injective ⇑f
x : R
hp : p ≠ 0
⊢ eval₂ f x p = 0 ↔ eval₂ f x p = 0

Tactic:
]

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

Goal state before:
pp: case mpr
σ : 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 : f = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
x : R
w : p ≠ 0
⊢ x ∈ p.roots ↔ x ∈ p.roots

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ p - q = 0

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ p - q = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ {p}

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ {p}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.natDegree ≠ 0
⊢ ∀ (b : R), ((fun x ↦ eval x p) ⁻¹' {b}).Finite

Tactic:
]

Goal state after:
R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.natDegree ≠ 0
⊢ ∀ (b : R), ((fun x ↦ eval x p) ⁻¹' {b}).Finite
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ a ~ᵤ p

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ a ~ᵤ p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : 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
⊢ q ∈ p ::ₘ s

Tactic:
by simp [hq]

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

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ d ∈ ↑(Finset.image (fun uv ↦ uv.1) (Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))))

Tactic:
]

Goal state after:
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ d ∈ ↑(Finset.image (fun uv ↦ uv.1) (Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))))
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
r : R
⊢ rootMultiplicity r p + rootMultiplicity r q = rootMultiplicity r p + rootMultiplicity r q

Tactic:
]

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
⊢ p * b ~ᵤ p * (normalizedFactors b).prod

Tactic:
]

Goal state after:
α : 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
⊢ p * b ~ᵤ p * (normalizedFactors b).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p k : R[X]
h : p * k ≠ 0
⊢ p.roots ≤ (p * k).roots

Tactic:
exact Multiset.le_iff_exists_add.mpr ⟨k.roots, roots_mul h⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a x : R
⊢ p ≠ C a ∧ eval x p = a ↔ p ≠ C a ∧ eval x p = a

Tactic:
]

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

Goal state before:
pp: case h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
x : σ
hd : d x ≤ n
⊢ (d + (equivFunOnFinite.symm (Function.const σ n) - d)) x = (equivFunOnFinite.symm (Function.const σ n)) x

Tactic:
]

Goal state after:
case h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
x : σ
hd : d x ≤ n
⊢ (d + (equivFunOnFinite.symm (Function.const σ n) - d)) x = (equivFunOnFinite.symm (Function.const σ n)) x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ (if s = r then 1 else 0) = if s = r then 1 else 0

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Multiset.Rel ?m.30 (normalizedFactors 1) 0

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Type ?u.21

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ α → ?m.29 → Prop

Tactic:
]

Goal state after:
case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Multiset.Rel ?m.30 (normalizedFactors 1) 0

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Type ?u.21

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ α → ?m.29 → Prop
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X.roots = X.roots

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
H : x = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
H : ¬x = 0
r : R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
x✝ : α
⊢ normalize x✝ = normalize x✝

Tactic:
]

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∑ x ∈ ?m.23, f x = ∑ i, f i

pp: case h
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ f.support ⊆ ?m.23

pp: case hf
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∀ x ∈ ?m.23, x ∉ f.support → f x = 0

pp: σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ Finset σ

Tactic:
]

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

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
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
]

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
⊢ p.roots = p.roots

Tactic:
]

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 = p.roots

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
⊢ ∀ (a_1 : R), count a_1 (Multiset.map f (p.comp (C a * X + C b)).roots) = count a_1 p.roots

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
⊢ ∀ (a_1 : R), count a_1 (Multiset.map f (p.comp (C a * X + C b)).roots) = count a_1 p.roots
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:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
x : R
⊢ rootMultiplicity (a * x + b) p = rootMultiplicity (f x) p

Tactic:
]

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

Goal state before:
pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ (normalizedFactors x).prod * (normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod

Tactic:
]

Goal state after:
case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ (normalizedFactors x).prod * (normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s = {x | degree x = n + 1 ∧ ↑x.support ⊆ s}

Tactic:
]

Goal state after:
case succ
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s = {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ {-(↑a⁻¹ * b)} = {-(↑a⁻¹ * b)}

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ hd.roots + (↑tl).bind roots = hd.roots + (↑tl).bind roots

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors x + n • normalizedFactors x = normalizedFactors x + n • normalizedFactors x

Tactic:
]

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ Multiset.replicate k (normalize p) = Multiset.replicate k (normalize p)

Tactic:
]

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

Goal state before:
pp: case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ n • p.roots + p.roots = n • p.roots + p.roots

Tactic:
]

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 ~ᵤ p * x

Tactic:
]

Goal state after:
α : 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 ~ᵤ p * x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ n • {0} = n • {0}

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih : (∀ a ∈ 0, Irreducible a) → normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ b ∈ 0, Irreducible b
⊢ {normalize a} = {normalize a}

Tactic:
]

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
⊢ fa.prod * fb.prod = fa.prod * fb.prod

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ s.val = s.val

Tactic:
]

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : (∀ a ∈ s, Irreducible a) → normalizedFactors s.prod = Multiset.map normalize s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ b ∈ s, Irreducible b
b : α
hb : b ∈ s
this : Nontrivial α
⊢ normalize a ::ₘ Multiset.map normalize s = normalize a ::ₘ Multiset.map normalize s

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a ↦ (X - C a).roots) = s

pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a ↦ X - C a) s

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a ↦ (X - C a).roots) = s

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a ↦ X - C a) s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ s = s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Rel ?m.19 (factors 1) 0

pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Type ?u.17

pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ α → ?m.18 → Prop

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Rel ?m.19 (factors 1) 0

α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Type ?u.17

α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ α → ?m.18 → Prop
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ¬∃ a ∈ s, X - C a = 0

Tactic:
]

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ¬∃ a ∈ s, X - C a = 0
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:
]

Goal state after:
α : 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
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (factors b)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (factors b))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x = normalizedFactors y
⊢ (normalizedFactors y).prod ~ᵤ (normalizedFactors y).prod

Tactic:
]

Goal state after: