mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ IsUnit k

Tactic:
;

Goal state after:
case cons.inl.refine_1.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ IsUnit k
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ IsUnit c

Tactic:
;

Goal state after:
case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ IsUnit c
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c * s.prod = x * y

Tactic:
;

Goal state after:
case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c * s.prod = x * y
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hc : x = c✝ * c
⊢ c✝ * c ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
;

Goal state after:
case cons.inr.inl
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hc : x = c✝ * c
⊢ c✝ * c ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ Prime c✝

Tactic:
;

Goal state after:
case cons.inr.inl.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ Prime c✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
h : WellFoundedLT (Associates α)
x✝¹ x✝ : Associates α
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
h : WellFoundedLT (Associates α)
x✝¹ x✝ : Associates α
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (p + C (-a)).degree = p.degree

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (p + C (-a)).degree = p.degree
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 α
h : Multiset.prod 0 ~ᵤ a
⊢ (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}

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 α
h : Multiset.prod 0 ~ᵤ a
⊢ (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
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

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), Prime x

Tactic:
;

Goal state after:
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

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), Prime x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ Prime x

Tactic:
;

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ Prime x
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 = ⊥

pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥

Tactic:
;

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

case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥
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

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), normalize x = x

Tactic:
;

Goal state after:
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

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), normalize x = x
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
⊢ 1 ≤ f i

Tactic:
;

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: case zero
σ : Type u_5
s : Set ℕ
hn : 0 ≠ 0
⊢ ⇑degree ⁻¹' (0 • s) = 0 • ⇑degree ⁻¹' s

pp: case succ
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n + 1) • s) = (n + 1) • ⇑degree ⁻¹' s

Tactic:
;

Goal state after:
case zero
σ : Type u_5
s : Set ℕ
hn : 0 ≠ 0
⊢ ⇑degree ⁻¹' (0 • s) = 0 • ⇑degree ⁻¹' s

case succ
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n + 1) • s) = (n + 1) • ⇑degree ⁻¹' s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ ∀ x_1 ∈ normalizedFactors (x * y), Irreducible x_1

Tactic:
exact irreducible_of_normalized_factor

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

Goal state before:
pp: case succ.refine_1
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ ∀ (b : α →₀ ℕ),
    degree b = n →
      (∀ (x : α), ¬b x = 0 → x ∈ s) → ∀ a ∈ s, degree b = n ∧ ∀ (x : α), (b x = 0 → ¬(single a 1) x = 0) → x ∈ s

Tactic:
;

Goal state after:
case succ.refine_1
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ ∀ (b : α →₀ ℕ),
    degree b = n →
      (∀ (x : α), ¬b x = 0 → x ∈ s) → ∀ a ∈ s, degree b = n ∧ ∀ (x : α), (b x = 0 → ¬(single a 1) x = 0) → x ∈ s
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.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.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ Rel Associated (factors (x ^ 0)) (0 • factors x)

Tactic:
rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p = 0
⊢ ↑(#S) ≠ p.degree

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p = 0
⊢ ↑(#S) ≠ p.degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ factors x ≠ 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ factors x ≠ 0
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:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (if 1 = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors 1)).prod) = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
q : R[X]
H : IsUnit q
hq : p = C 0 * q
⊢ False

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
q : R[X]
H : IsUnit q
hq : p = C 0 * q
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
h₁ : X ^ 2 - C 1 = (X + C 1) * (X - C 1)
h₂ : X ^ 2 - C 1 ≠ 0
⊢ {-1} + {1} = {-1, 1}

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
h₁ : X ^ 2 - C 1 = (X + C 1) * (X - C 1)
h₂ : X ^ 2 - C 1 ≠ 0
⊢ {-1} + {1} = {-1, 1}
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

pp: case neg
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:
;

Goal state after:
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

case neg
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
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)

pp: case neg
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:
;

Goal state after:
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)

case neg
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)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x ↦ r * p.coeff x

Tactic:
;

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x ↦ r * p.coeff x
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
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ b ≠ 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ b ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e w.prod * ↑((Units.map e.toMonoidHom) u) = a

Tactic:
toMonoidHom_eq_coe,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e w.prod * ↑((Units.map ↑e) u) = a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
x✝ : R
⊢ x✝ ∈ (fun x ↦ eval x p) ⁻¹' {a} ↔ x✝ ∈ (p - C a).rootSet R

Tactic:
;

Goal state after:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
x✝ : R
⊢ x✝ ∈ (fun x ↦ eval x p) ⁻¹' {a} ↔ x✝ ∈ (p - C a).rootSet R
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p = C p.content * p.primPart

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * p.primPart

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p = C p.content * p.primPart

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h✝ : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
h : derivative p = 0
⊢ (X - C t) ^ m ∣ 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h✝ : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
h : derivative p = 0
⊢ (X - C t) ^ m ∣ 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.IsPrimitive

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.IsPrimitive

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive
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
⊢ ↑m ! * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) = ↑m ! * eval t (p /ₘ (X - C t) ^ m)

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ↑m ! * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) = ↑m ! * eval t (p /ₘ (X - C t) ^ m)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ count r s ≤ rootMultiplicity r p

Tactic:
le_rootMultiplicity_iff hp,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (X - C r) ^ count r s ∣ p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
apply lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑n ! ∈ nonZeroDivisors R
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 ∈ nonZeroDivisors R

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 ∈ nonZeroDivisors R
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

pp: case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
· rw [h, map_zero, rootMultiplicity_zero]

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hdf0 : derivative f ≠ 0
hr : derivative f * 0 = f * r
hg : ¬IsRoot 0 a
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hdf0 : derivative f ≠ 0
hr : derivative f * 0 = f * r
hg : ¬IsRoot 0 a
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ FactorSetMem ⊤ p

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ FactorSetMem ⊤ p