awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : ∀ a ∈ s, Irreducible a
empty :
  ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Irreducible a),
    Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
      (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
cons :
  ∀ (a : α) (s : Multiset α)
    (ih : ∀ (hs : ∀ a ∈ s, Irreducible a), normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s)
    (hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1),
    normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
⊢ normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s

Tactic:
induction s using Multiset.induction with
  | empty => rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
  | cons a s ih =>
    have ia := hs a (Multiset.mem_cons_self a _)
    have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
    obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
    · rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
    haveI := nontrivial_of_ne b 0 (ib b hb).ne_zero
    rw [Multiset.prod_cons, Multiset.map_cons,
      normalizedFactors_mul ia.ne_zero (Multiset.prod_ne_zero fun h => (ib 0 h).ne_zero rfl),
      normalizedFactors_irreducible ia, ih ib, Multiset.singleton_add]

Premises used: Multiset.prod_zero, Multiset.singleton_add, Multiset.map_singleton, Multiset.map_cons, Multiset.prod_cons, Multiset.map_zero, UniqueFactorizationMonoid.normalizedFactors_one, Multiset.prod_singleton, Multiset.cons_zero, Multiset.empty_or_exists_mem, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
mp : x ∣ y → normalizedFactors x ≤ normalizedFactors y
mpr : normalizedFactors x ≤ normalizedFactors y → x ∣ y
⊢ x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
c : α
hy : x * c ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors (x * c)

Tactic:
simp [hx, right_ne_zero_of_mul hy]

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
mpr : normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod
⊢ normalizedFactors x ≤ normalizedFactors y → x ∣ y

Tactic:
rw [← (prod_normalizedFactors hx).dvd_iff_dvd_left, ←
      (prod_normalizedFactors hy).dvd_iff_dvd_right]

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors, Associated.dvd_iff_dvd_left, Associated.dvd_iff_dvd_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod

Tactic:
apply Multiset.prod_dvd_prod_of_le

Premises used: Multiset.prod_dvd_prod_of_le
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)

Tactic:
have h' : ⇑(normalize (α := α)) = Associates.out ∘ Associates.mk := funext Associates.out_mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
rw :
  Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors a) =
    Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
rw₁ :
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
rw₂ :
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors b))
rw₃ rw₄ :
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors b)) =
    Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors b))
⊢ Eq (α := Multiset α) (Multiset.map (⇑normalize : (a : α) → α) (factors a))
    (Multiset.map (⇑normalize : (a : α) → α) (factors b))

Tactic:
rw [h', ← Multiset.map_map, ← Multiset.map_map,
    Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]

Premises used: UniqueFactorizationMonoid.factors_rel_of_associated, Associates.rel_associated_iff_map_eq_map, Iff.mp, Multiset.map_map
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x = normalizedFactors y
rw rw₁ : (normalizedFactors y).prod ~ᵤ (normalizedFactors y).prod
⊢ (normalizedFactors x).prod ~ᵤ (normalizedFactors y).prod

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
rw : k • normalizedFactors p = Multiset.replicate k ((normalize : (a : α) → α) p)
rw₁ :
  HSMul.hSMul (β := Multiset α) k (singleton (α := α) ((normalize : (a : α) → α) p : α)) =
    Multiset.replicate k ((normalize : (a : α) → α) p)
rw₂ rw₃ :
  Eq (α := Multiset α) (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
    (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)

Tactic:
rw [normalizedFactors_pow, normalizedFactors_irreducible hp, Multiset.nsmul_singleton]

Premises used: UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
⊢ 0 ∉ normalizedFactors x

Tactic:
fun h =>
  Prime.ne_zero (prime_of_normalized_factor _ h) rfl

Premises used: UniqueFactorizationMonoid.prime_of_normalized_factor, Prime.ne_zero, OfNat.ofNat, Not, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x a : α
hx : x ∈ normalizedFactors a
⊢ x ≠ 0

Tactic:
ne_of_mem_of_not_mem hx <| zero_notMem_normalizedFactors a

Premises used: ne_of_mem_of_not_mem, UniqueFactorizationMonoid.zero_notMem_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
pos : ∀ (hcases : a = 0), p ∣ a
neg : ∀ (hcases : ¬a = 0), p ∣ a
⊢ p ∣ a

Tactic:
by_cases hcases : a = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
pos : p ∣ 0
⊢ p ∣ a

Tactic:
rw [hcases]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ 0

Tactic:
dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ 0

Tactic:
exact dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : ¬a = 0
⊢ p ∣ a

Tactic:
dvd_trans (Multiset.dvd_prod H) (Associated.dvd (prod_normalizedFactors hcases))

Premises used: Associated.dvd, Multiset.dvd_prod, dvd_trans, UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : ¬a = 0
⊢ p ∣ a

Tactic:
exact dvd_trans (Multiset.dvd_prod H) (Associated.dvd (prod_normalizedFactors hcases))

Premises used: Associated.dvd, Multiset.dvd_prod, dvd_trans, UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
mp : p ∈ normalizedFactors x → Prime p ∧ p ∣ x
mpr : Prime p ∧ p ∣ x → p ∈ normalizedFactors x
⊢ p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
h : p ∈ normalizedFactors x
⊢ Prime p ∧ p ∣ x

Tactic:
⟨prime_of_normalized_factor p h, dvd_of_mem_normalizedFactors h⟩

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, UniqueFactorizationMonoid.prime_of_normalized_factor, And.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
h : p ∈ normalizedFactors x
⊢ Prime p ∧ p ∣ x

Tactic:
exact ⟨prime_of_normalized_factor p h, dvd_of_mem_normalizedFactors h⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
mpr : ∀ (q : α) (hqmem : q ∈ normalizedFactors x) (hqeq : p ~ᵤ q), p ∈ normalizedFactors x
⊢ p ∈ normalizedFactors x

Tactic:
obtain ⟨q, hqmem, hqeq⟩ := exists_mem_normalizedFactors_of_dvd hx hprime.irreducible hdvd

Premises used: Prime.irreducible, UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p ~ᵤ q
⊢ p = q

Tactic:
rw [associated_iff_eq] at hqeq

Premises used: associated_iff_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p = q
⊢ p ∈ normalizedFactors x

Tactic:
hqeq ▸ hqmem

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p = q
⊢ p ∈ normalizedFactors x

Tactic:
exact hqeq ▸ hqmem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
⊢ p ∈ normalizedFactors x ↔ Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x

Tactic:
⟨fun h ↦ ⟨irreducible_of_normalized_factor p h, normalize_normalized_factor p h,
    dvd_of_mem_normalizedFactors h⟩, fun ⟨h₁, h₂, h₃⟩ ↦ ?_⟩

Premises used: UniqueFactorizationMonoid.normalizedFactors, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, UniqueFactorizationMonoid.normalize_normalized_factor, _private.0.UniqueFactorizationMonoid.mem_normalizedFactors_iff'.match_1, Membership.mem, And.intro, Iff.intro, UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
refine :
  Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x →
    ∀ (h₁ : Irreducible p) (h₂ : (normalize : (a : α) → α) p = p) (h₃ : p ∣ x), p ∈ normalizedFactors x
⊢ p ∈ normalizedFactors x ↔ Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x

Tactic:
refine ⟨fun h ↦ ⟨irreducible_of_normalized_factor p h, normalize_normalized_factor p h,
    dvd_of_mem_normalizedFactors h⟩, fun ⟨h₁, h₂, h₃⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
h_1 : Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : (normalize : (a : α) → α) p = p
h₃ : p ∣ x
obtain : ∀ (y : α) (hy₁ : y ∈ factors x) (hy₂ : p ~ᵤ y), p ∈ normalizedFactors x
⊢ p ∈ normalizedFactors x

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := exists_mem_factors_of_dvd h h₁ h₃

Premises used: UniqueFactorizationMonoid.exists_mem_factors_of_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
h_1 : Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : (normalize : (a : α) → α) p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
rwa : Eq (α := α) ((normalize : (a : α) → α) y : α) ((normalize : (a : α) → α) p : α)
rwa₁ : y ~ᵤ p
rwa₂ rwa₃ rwa₄ rwa₅ : p ~ᵤ y
⊢ (normalize : (a : α) → α) y = p

Tactic:
rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]

Premises used: Associated.comm, normalize_eq_normalize_iff_associated
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
h_1 : Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : (normalize : (a : α) → α) p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ p ∈ normalizedFactors x

Tactic:
exact Multiset.mem_map.mpr ⟨y, hy₁, by
    rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]⟩

Premises used: Iff.mpr, Multiset.mem_map, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
rw : ∀ {a_1 : α}, a_1 ∈ normalizedFactors a → a_1 ∉ normalizedFactors b
⊢ Disjoint (normalizedFactors a) (normalizedFactors b)

Tactic:
rw [Multiset.disjoint_left]

Premises used: Multiset.disjoint_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
⊢ x ∣ a

Tactic:
have x_dvd_a := dvd_of_mem_normalizedFactors hxa
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
⊢ x ∣ b

Tactic:
have x_dvd_b := dvd_of_mem_normalizedFactors hxb
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
x_dvd_b : x ∣ b
⊢ False

Tactic:
(prime_of_normalized_factor x hxa).not_unit (hc x_dvd_a x_dvd_b)

Premises used: Prime.not_unit, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
x_dvd_b : x ∣ b
⊢ False

Tactic:
exact (prime_of_normalized_factor x hxa).not_unit (hc x_dvd_a x_dvd_b)

Premises used: Prime.not_unit, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
h₁ : p ^ (normalizedFactors r).card ~ᵤ r
⊢ ∃ (i : ℕ), p ^ i ~ᵤ r

Tactic:
use (normalizedFactors r).card

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.card
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ (normalizedFactors r).prod ~ᵤ r

Tactic:
have := UniqueFactorizationMonoid.prod_normalizedFactors hr
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (normalizedFactors r).prod ~ᵤ r
h₁ : ∀ (this : (Multiset.replicate (normalizedFactors r).card p).prod ~ᵤ r), p ^ (normalizedFactors r).card ~ᵤ r
h₂ h₃ h₄ h₅ : ∀ (this : p ^ (normalizedFactors r).card ~ᵤ r), p ^ (normalizedFactors r).card ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r

Tactic:
rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this

Premises used: Multiset.prod_replicate, Multiset.eq_replicate_of_mem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
inl : Subsingleton α → normalizedFactors m.prod = m
inr : Nontrivial α → normalizedFactors m.prod = m
⊢ normalizedFactors m.prod = m

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h_1 : Subsingleton α
⊢ m = 0

Tactic:
Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_

Premises used: Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h_1 : Subsingleton α
refine : ∀ (x : α) (hx : x ∈ m), False
⊢ m = 0

Tactic:
refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_

Premises used: Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h_1 : Subsingleton α
x : α
hx : x ∈ m
⊢ False

Tactic:
simpa [Subsingleton.elim x 0] using h x hx

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h_1 : Subsingleton α
inl :
  ∀ (h : ∀ (p : α), Membership.mem (γ := Multiset α) 0 p → Prime p),
    Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0)) 0
⊢ normalizedFactors m.prod = m

Tactic:
obtain rfl : m = 0 := by
      refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx

Premises used: rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
h_1 : Subsingleton α
h : ∀ (p : α), Membership.mem (γ := Multiset α) 0 p → Prime p
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h_1 : Nontrivial α
⊢ normalizedFactors m.prod = m

Tactic:
simpa only [← Multiset.rel_eq, ← associated_eq_eq] using
      prime_factors_unique prime_of_normalized_factor h
        (prod_normalizedFactors (m.prod_ne_zero_of_prime h))

Premises used: associated_eq_eq, UniqueFactorizationMonoid.prime_of_normalized_factor, Multiset.prod_ne_zero_of_prime, prime_factors_unique, UniqueFactorizationMonoid.prod_normalizedFactors, Multiset.rel_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
rw : a ∣ b ∧ b ∣ a
⊢ a = b

Tactic:
rw [← normalize_normalized_factor a ha, ← normalize_normalized_factor b hb,
    normalize_eq_normalize_iff]

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor, normalize_eq_normalize_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ a ∣ b ∧ b ∣ a

Tactic:
Associated.dvd_dvd h

Premises used: Associated.dvd_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ a ∣ b ∧ b ∣ a

Tactic:
exact Associated.dvd_dvd h

Premises used: Associated.dvd_dvd