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

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

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

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h✝ : Subsingleton α
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ ∀ x ∈ s, Irreducible x

pp: case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ t.prod ~ᵤ s.prod

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ ∀ x ∈ s, Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

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

pp: case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

pp: case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0

Tactic:
·

Goal state after:
case inr.cons
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ 0 ∉ s✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

pp: case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0

Tactic:
·

Goal state after:
case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0

Tactic:
·

Goal state after:
case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
a x : α
ha : a ≠ 0
⊢ x ∈ normalizedFactors a ↔ ↑f x ∈ normalizedFactors (f a)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : n = 0
⊢ f x ∈ nthRootsFinset n (f a)

pp: case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
⊢ f x ∈ nthRootsFinset n (f a)

Tactic:
·

Goal state after:
case pos
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : n = 0
⊢ f x ∈ nthRootsFinset n (f a)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

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

Tactic:
simp [mem_normalizedFactors_iff' ha,
        mem_normalizedFactors_iff' (EmbeddingLike.map_ne_zero_iff.mpr ha), map_dvd_iff_dvd_symm,
        MulEquiv.irreducible_iff, he]

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

Goal state before:
pp: case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
⊢ f x ∈ nthRootsFinset n (f a)

Tactic:
·

Goal state after:
case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
⊢ f x ∈ nthRootsFinset n (f a)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : x = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : x = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
⊢ Irreducible x

pp: case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
⊢ Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : x = 0
⊢ Associates.mk (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) = x

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
⊢ Associates.mk (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) = x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : x = 0
⊢ Associates.mk (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) = x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ p
⊢ Irreducible x

pp: case refine_1.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ factors c
⊢ Irreducible x

Tactic:
·

Goal state after:
case refine_1.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ p
⊢ Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ factors c
⊢ Irreducible x

Tactic:
·

Goal state after:
case refine_1.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ factors c
⊢ Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ 0

Tactic:
apply dvd_zero

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ α → ℕ∞

pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∀ {a b : α}, DvdNotUnit a b → ?refine_1 a < ?refine_1 b

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ α → ℕ∞
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : a = 0
⊢ ℕ∞

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : ¬a = 0
⊢ ℕ∞

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : a = 0
⊢ ℕ∞
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬(X * p).coeff 0 = 0 ↔ ∃ a, ¬p.coeff a = 0 ∧ a.succ = 0

pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff (a + 1) = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬(X * p).coeff 0 = 0 ↔ ∃ a, ¬p.coeff a = 0 ∧ a.succ = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos
α : 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
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

pp: case neg
α : 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
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
·

Goal state after:
case pos
α : 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
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card
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
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

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
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case succ.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 → ∃ a_2, ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1

pp: case succ.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0

Tactic:
·

Goal state after:
case succ.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 → ∃ a_2, ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case succ.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0

Tactic:
·

Goal state after:
case succ.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0
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
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg.calc_1
α : 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
con : Classical.choose ⋯ = 0
⊢ c ~ᵤ 1

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 ∈ Classical.choose ⋯ + Classical.choose ⋯, Prime x

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 ⋯ + Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod

Tactic:
·

Goal state after:
case neg.calc_1
α : 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
con : Classical.choose ⋯ = 0
⊢ c ~ᵤ 1