mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

pp: case cons.inr.inr
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 : y = c✝ * c
⊢ x ∈ 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
⊢ x ∈ 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
⊢ c✝ ∈ {r | IsUnit r ∨ Prime r}

pp: case cons.inr.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}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

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
⊢ c✝ ∈ {r | IsUnit r ∨ Prime r}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

pp: case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
·

Goal state after:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
·

Goal state after:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ f s • w s

pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
·

Goal state after:
σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ f s • w s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b = 0
⊢ (factors a).card = (factors b).card

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : ¬b = 0
⊢ (factors a).card = (factors b).card

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b = 0
⊢ (factors a).card = (factors b).card
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
·

Goal state after:
σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p = 0
⊢ p.roots.card ≤ p.natDegree

pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p = 0
⊢ p.roots.card ≤ p.natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case e_f
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ (Associates.mk ∘ normalize) x✝ = Associates.mk x✝

Tactic:
rw [Function.comp_apply, Associates.mk_normalize]

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize (normalizedFactors a).prod

pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a

Tactic:
·

Goal state after:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize (normalizedFactors a).prod
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:
by rw [sub_eq_add_neg, ← C_neg]; exact degree_add_C hp0

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a

Tactic:
·

Goal state after:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p = 0
⊢ count a p.roots = rootMultiplicity a p

pp: case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a p.roots = rootMultiplicity a p

Tactic:
·

Goal state after:
case pos
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p = 0
⊢ count a p.roots = rootMultiplicity a p
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 α
⊢ Multiset.prod 0 ~ᵤ a → (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}

pp: case refine_2
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}) →
      (a_1 ::ₘ s).prod ~ᵤ a → (∀ b ∈ a_1 ::ₘ s, Prime b) → ∃ p, a ~ᵤ p ∧ a_1 ::ₘ s = {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 α
⊢ Multiset.prod 0 ~ᵤ a → (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ (weight w) f = 0 → f = 0

pp: case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ f = 0 → (weight w) f = 0

Tactic:
·

Goal state after:
case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ (weight w) f = 0 → f = 0
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
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 = ⊥
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ f = 0 → (weight w) f = 0

Tactic:
·

Goal state after:
case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ f = 0 → (weight w) f = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}) →
      (a_1 ::ₘ s).prod ~ᵤ a → (∀ b ∈ a_1 ::ₘ s, Prime b) → ∃ p, a ~ᵤ p ∧ a_1 ::ₘ s = {p}

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}) →
      (a_1 ::ₘ s).prod ~ᵤ a → (∀ b ∈ a_1 ::ₘ s, Prime b) → ∃ p, a ~ᵤ p ∧ a_1 ::ₘ s = {p}
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
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

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

pp: case refine_2
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit (p * ↑u * (s.erase q).prod)

Tactic:
·

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ normalizedFactors 1 = 0

pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ normalizedFactors 1 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ ∀ x ∈ 0, Irreducible x

pp: case inr.h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ (normalizedFactors 1).prod ~ᵤ Multiset.prod 0

Tactic:
·

Goal state after:
case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ ∀ x ∈ 0, Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ (normalizedFactors 1).prod ~ᵤ Multiset.prod 0

Tactic:
·

Goal state after:
case inr.h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ (normalizedFactors 1).prod ~ᵤ Multiset.prod 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ f s ≤ degree f

pp: case neg
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ degree f

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ f s ≤ degree f
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ degree f

Tactic:
·

Goal state after:
case neg
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ degree f
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case refine_1
σ : Type u_1
⊢ (Set.range fun a ↦ single a 1) ⊆ {d | degree d = 1}

pp: case refine_2
σ : Type u_1
⊢ {d | degree d = 1} ⊆ Set.range fun a ↦ single a 1

Tactic:
·

Goal state after:
case refine_1
σ : Type u_1
⊢ (Set.range fun a ↦ single a 1) ⊆ {d | degree d = 1}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case refine_2
σ : Type u_1
⊢ {d | degree d = 1} ⊆ Set.range fun a ↦ single a 1

Tactic:
·

Goal state after:
case refine_2
σ : Type u_1
⊢ {d | degree d = 1} ⊆ Set.range fun a ↦ single a 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hf
α : 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 + normalizedFactors y, Irreducible x_1

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

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

Tactic:
·

Goal state after:
case hf
α : 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 + normalizedFactors y, Irreducible x_1
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_5
f : σ →₀ ℕ
n : ℕ
IH : n ≤ degree f → ∃ g ≤ f, degree g = n
hn : n + 1 ≤ degree f
⊢ n ≤ degree f

Tactic:
by lia

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

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

Tactic:
·

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

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

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x
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}
⊢ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s ⊆ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}

pp: case succ.refine_2
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
f : α →₀ ℕ
x✝ : f ∈ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
f_deg : degree f = n + 1
f_supp : ↑f.support ⊆ s
⊢ f ∈ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' 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}
⊢ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s ⊆ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}