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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos.refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * b = p * b

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ C r = C r

Tactic:
]

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
⊢ eval t (m.choose 0 • ((⇑derivative)^[m - 0] ((X - C t) ^ m) * (⇑derivative)^[0] (p /ₘ (X - C t) ^ m))) =
    m ! • eval t (p /ₘ (X - C t) ^ m)

pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∀ b ∈ range m.succ,
    b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0

Tactic:
]

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

R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∀ b ∈ range m.succ,
    b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ p - q = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ p - q = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : NormalizedGCDMonoid R
S : Type u_2
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
inst✝¹ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
inst✝ : Nontrivial S
⊢ (aeval s) p.primPart = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : NormalizedGCDMonoid R
S : Type u_2
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
inst✝¹ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
inst✝ : Nontrivial S
⊢ (aeval s) p.primPart = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : NormalizedGCDMonoid R
S : Type u_2
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
inst✝¹ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
inst✝ : Nontrivial S
this : IsDomain R
⊢ ¬p = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : NormalizedGCDMonoid R
S : Type u_2
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
inst✝¹ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
inst✝ : Nontrivial S
this : IsDomain R
⊢ ¬p = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : f p.content * eval₂ f s p.primPart = 0
⊢ eval₂ f s p.primPart = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : f p.content * eval₂ f s p.primPart = 0
⊢ eval₂ f s p.primPart = 0
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.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : f p.content * eval₂ f s p.primPart = 0
⊢ ¬p = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : f p.content * eval₂ f s p.primPart = 0
⊢ ¬p = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) = gcd a q.content

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) = gcd a q.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ s.1.prod ∣ (normalizedFactors y).prod

Tactic:
]

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ s.1.prod ∣ (normalizedFactors y).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : y = 0
hx : x = 0
⊢ y = 0

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : y = 0
hx : x = 0
⊢ y = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ map (algebraMap R (FractionRing R)) (Multiset.map (fun a ↦ X - C a) p.roots).prod ∣
    map (algebraMap R (FractionRing R)) p

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ map (algebraMap R (FractionRing R)) (Multiset.map (fun a ↦ X - C a) p.roots).prod ∣
    map (algebraMap R (FractionRing R)) p
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ ∏ i ∈ p.roots.toFinset, map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p) ∣
    map (algebraMap R (FractionRing R)) p

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ ∏ i ∈ p.roots.toFinset, map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p) ∣
    map (algebraMap R (FractionRing R)) p
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ a * w.coeff x = a * w.coeff x

Tactic:
]

Goal state after:
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.leadingCoeff (p * q).eraseLead.content = gcd p.leadingCoeff (p.eraseLead * q).content

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd p.leadingCoeff (p * q).eraseLead.content = gcd p.leadingCoeff (p.eraseLead * q).content
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * (C q.leadingCoeff * X ^ (p * q).natDegree)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * (C q.leadingCoeff * X ^ (p * q).natDegree)
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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
suffices h : ∀ (n : ℕ) (p q : R[X]),
        (p * q).degree < n → Associated ((p * q).content) (p.content * q.content) by
      apply h
      apply lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 (Nat.lt_succ_self _))

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
⊢ ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
p q : R[X]
hpq : p = 0 ∨ q = 0
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
]

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
p q : R[X]
hpq : p = 0 ∨ q = 0
⊢ Associated (p * q).content (p.content * q.content)
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
⊢ (Multiset.map (fun a ↦ X - C a) (Multiset.filter (Eq r) s)).prod ∣ p

Tactic:
]

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
⊢ (Multiset.map (fun a ↦ X - C a) (Multiset.filter (Eq r) s)).prod ∣ p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p)! • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p)! • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val a).prod * (Multiset.map Subtype.val b).prod =
    (Multiset.map Subtype.val a).prod * (Multiset.map Subtype.val b).prod

Tactic:
]

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

Goal state before:
pp: case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0

Tactic:
]

Goal state after:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1) ∈ nonZeroDivisors R ∧ ↑n ! ∈ nonZeroDivisors R

Tactic:
]

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1) ∈ 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: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ (∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t) ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ (∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t) ↔ p.IsRoot t ∧ (derivative p).IsRoot t
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
⊢ 0 = 0 - 1

Tactic:
]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)

Tactic:
]

Goal state after:
case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : C (f.coeff 0) ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬(C (f.coeff 0)).IsRoot a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : (p * q).degree < ↑n ∨ p.natDegree + q.natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : (p * q).degree < ↑n ∨ p.natDegree + q.natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.roots.card + q.natDegree

Tactic:
]

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

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

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
this : IsDomain R
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : p.roots + q.roots = p.roots
⊢ q.roots = 0

pp: case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).roots = p.roots
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod * q ≠ 0

Tactic:
]

Goal state after:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : p.roots + q.roots = p.roots
⊢ q.roots = 0

case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).roots = p.roots
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod * q ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : False
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : False
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C (↑w * ↑w⁻¹) * C ↑(normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)

Tactic:
]

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C (↑w * ↑w⁻¹) * C ↑(normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ ↑(normUnit (a✝ * b✝)) = ↑(normUnit a✝) * ↑(normUnit b✝)

Tactic:
]

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ ↑(normUnit (a✝ * b✝)) = ↑(normUnit a✝) * ↑(normUnit b✝)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
]

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case coe.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ 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]
hp : p.Monic
hroots : p.roots.card = p.natDegree
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod = (Multiset.map (fun a ↦ X - C a) p.roots).prod

Tactic:
]

Goal state after: