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

Goal state before:
pp: case neg.calc_2
α : 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
x : α
hadd : x ∈ Classical.choose ⋯ ∨ x ∈ Classical.choose ⋯
⊢ Prime x

Tactic:
]

Goal state after:
case neg.calc_2
α : 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
x : α
hadd : x ∈ Classical.choose ⋯ ∨ x ∈ Classical.choose ⋯
⊢ Prime x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ p * q ≠ 0

Tactic:
]

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ p * q ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
r : T
⊢ {(algebraMap T S) r} = {(algebraMap T S) r}

Tactic:
]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ {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
r : R
k : ℕ
⊢ Associated (C r * X ^ k).content r

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated (C r * X ^ k).content r
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ 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
r : R
k : ℕ
⊢ Associated r r

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated r r
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg.calc_3
α : 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
⊢ (Classical.choose ⋯).prod * (Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod

Tactic:
]

Goal state after:
case neg.calc_3
α : 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
⊢ (Classical.choose ⋯).prod * (Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
⊢ (map (algebraMap T S) p).roots = p.aroots S

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (map (algebraMap T S) p).roots = p.aroots S

pp: case ha
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (algebraMap T S) a ≠ 0

Tactic:
]

Goal state after:
case ha
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (algebraMap T S) a ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case ha
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ a ≠ 0

pp: case ha.hf
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ Function.Injective ⇑(algebraMap T S)

Tactic:
]

Goal state after:
case ha
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ a ≠ 0

case ha.hf
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ Function.Injective ⇑(algebraMap T S)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ p.content = p.content

Tactic:
]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ p.aroots S = p.aroots S

Tactic:
]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
n : ℕ
⊢ n • (map (algebraMap T S) p).roots = n • p.aroots S

Tactic:
]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
n : ℕ
⊢ n • {0} = n • {0}

Tactic:
]

Goal state after:
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 ~ᵤ (Classical.choose ⋯).prod

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 ~ᵤ (Classical.choose ⋯).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ n • {0} = n • {0}

Tactic:
]

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

Goal state before:
pp: case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∀ b ∈ Finset.range n, p.content ∣ p.coeff b

Tactic:
]

Goal state after:
case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∀ b ∈ Finset.range n, p.content ∣ p.coeff b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map ((algebraMap S R).comp (algebraMap T S)) p).roots = (map ((algebraMap S R).comp (algebraMap T S)) p).roots

Tactic:
]

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

Goal state before:
pp: T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ ↑(p.aroots S).toFinset = ↑(p.aroots S).toFinset

Tactic:
]

Goal state after:
T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ ↑(p.aroots S).toFinset = ↑(p.aroots S).toFinset
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ ∅ = ∅

Tactic:
]

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ ∅ = ∅

Tactic:
]

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ ↑(p.aroots S).toFinset = ↑(p.aroots S).toFinset

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
p : R[X]
h : p.natDegree ∈ p.support
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p
⊢ Prime q

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p
⊢ Prime q
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 : β), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
]

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 : β), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
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
⊢ ¬(X - C t) ^ (m - 1) * (X - C t) ∣ C ↑(m - 1 + 1) * (X - C t) ^ (m - 1 + 1 - 1) * g

Tactic:
hm,

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
⊢ ¬(X - C t) ^ (m - 1) * (X - C t) ∣ C ↑m * (X - C t) ^ (m - 1) * g
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0 ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

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
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.coeff i

Tactic:
]

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

Goal state before:
pp: T : Type w
inst✝⁵ : CommRing T
p : T[X]
S : Type u_1
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : S
⊢ p ≠ 0 ∧ (aeval a) p = 0 ↔ p ≠ 0 ∧ (aeval a) p = 0

Tactic:
]

Goal state after:
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
⊢ ¬X - C t ∣ C ↑m * g

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
⊢ ¬X - C t ∣ C ↑m * g
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i
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
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : UniqueFactorizationMonoid α
⊢ UniqueFactorizationMonoid β

Tactic:
have := e.isCancelMulZero_iff.mp inferInstance
  rw [UniqueFactorizationMonoid.iff_exists_prime_factors] at hα ⊢
  intro a ha
  obtain ⟨w, hp, u, h⟩ :=
    hα (e.symm a) fun h =>
      ha <| by
        convert! ← map_zero e
        simp [← h]
  exact
    ⟨w.map e, fun b hb =>
        let ⟨c, hc, he⟩ := Multiset.mem_map.1 hb
        he ▸ (prime_iff e).2 (hp c hc),
        Units.map e.toMonoidHom u,
      by
        rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]⟩

Goal state after:
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 : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬eval t (C ↑m * g) = 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 : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬eval t (C ↑m * g) = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ (aeval (f x)) p = 0

Tactic:
]

Goal state after:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ (aeval (f x)) p = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ ∀ b ∈ p.support, r ∣ p.coeff b

Tactic:
]

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ ∀ b ∈ p.support, r ∣ p.coeff b
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 : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬eval t g = 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 : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬eval t g = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ 0 = 0

Tactic:
]

Goal state after:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ ∅
hf : p = 0
⊢ False

Tactic:
]

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ ∅
hf : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
]

Goal state after:
T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S') p = 0
Module: Mathlib.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 neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = p

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
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.IsPrimitive

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.IsPrimitive
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ IsUnit p.primPart.content
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
hnezero : derivative p ≠ 0
⊢ ¬(X - C t) ^ m ∣ derivative p

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
hnezero : derivative p ≠ 0
⊢ ¬(X - C t) ^ m ∣ derivative p
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : p = 0
⊢ p.primPart.natDegree = p.natDegree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
⊢ p = p

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case pos.refine_1
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 * a = p * a

Tactic:
]

Goal state after: