awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
e_a : Eq.{u_1 + 1} (α := α → Associates α) (Associates.mk ∘ (⇑normalize : (a : α) → α)) Associates.mk
⊢ Eq (α := Associates α)
    (Multiset.prod
      (Multiset.map (Associates.mk ∘ (⇑normalize : (a : α) → α))
        (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)))
    (Multiset.prod
      (Multiset.map Associates.mk (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)))

Tactic:
congr 2
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
e_a : ∀ (x : α), Eq (α := Associates α) ((Associates.mk ∘ (⇑normalize : (a : α) → α)) x) (Associates.mk x)
⊢ Eq.{u_1 + 1} (α := α → Associates α) (Associates.mk ∘ (⇑normalize : (a : α) → α)) Associates.mk

Tactic:
ext
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x : α
e_a :
  Eq (α := Associates α) (Associates.mk ((normalize : (a : α) → α) x) : Associates α) (Associates.mk x : Associates α)
e_a₁ e_a₂ : Eq (α := Associates α) (Associates.mk x) (Associates.mk x)
⊢ Eq (α := Associates α) ((Associates.mk ∘ (⇑normalize : (a : α) → α)) x) (Associates.mk x)

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

Premises used: Associates.mk_normalize, Function.comp_apply
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
trans : (normalizedFactors a).prod = (normalize : (a : α) → α) (normalizedFactors a).prod
trans₁ : Eq (α := α) ((normalize : (a : α) → α) (normalizedFactors a).prod : α) ((normalize : (a : α) → α) a : α)
⊢ (normalizedFactors a).prod = (normalize : (a : α) → α) a

Tactic:
trans normalize (normalizedFactors a).prod

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.prod, normalize, DFunLike.coe
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
rw :
  Eq (α := α) (Multiset.prod (Multiset.map (⇑normalize : (a : α) → α) (factors a)) : α)
    ((normalize : (a : α) → α) (Multiset.prod (Multiset.map (⇑normalize : (a : α) → α) (factors a))) : α)
rw₁ :
  Eq (α := α) ((normalize : (a : α) → α) (factors a).prod : α)
    ((normalize : (a : α) → α) ((normalize : (a : α) → α) (factors a).prod : α) : α)
rw₂ rw₃ : Eq (α := α) ((normalize : (a : α) → α) (factors a).prod : α) ((normalize : (a : α) → α) (factors a).prod : α)
⊢ (normalizedFactors a).prod = (normalize : (a : α) → α) (normalizedFactors a).prod

Tactic:
rw [normalizedFactors, ← map_multiset_prod, normalize_idem]

Premises used: UniqueFactorizationMonoid.normalizedFactors, map_multiset_prod, normalize_idem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Eq (α := α) ((normalize : (a : α) → α) (normalizedFactors a).prod : α) ((normalize : (a : α) → α) a : α)

Tactic:
normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

Premises used: Iff.mpr, normalize_eq_normalize_iff, dvd_dvd_iff_associated, UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Eq (α := α) ((normalize : (a : α) → α) (normalizedFactors a).prod : α) ((normalize : (a : α) → α) a : α)

Tactic:
exact normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

Premises used: Iff.mpr, normalize_eq_normalize_iff, dvd_dvd_iff_associated, UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
pos :
  ∀ (ane0 : a = 0) (x : α),
    Membership.mem (γ := Multiset α) (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x) 0) x → Prime x
neg :
  ∀ (ane0 : ¬a = 0) (x : α),
    Membership.mem (γ := Multiset α)
        (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
          (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
        x →
      Prime x
⊢ ∀ (x : α),
    Membership.mem (γ := Multiset α)
        (Multiset.map (α := α) (⇑normalize : (a : α) → α)
          (if h : a = 0 then 0 else Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
        x →
      Prime x

Tactic:
split_ifs with ane0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a = 0
⊢ ∀ (x : α), Membership.mem (γ := Multiset α) (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x) 0) x → Prime x

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
x : α
hx :
  Membership.mem (γ := Multiset α)
    (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
      (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
    x
neg :
  ∀ (y : α) (hy : y ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)
    (hx :
      Membership.mem (α := α) (γ := Multiset α)
        (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
          (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
        ((normalize : (a : α) → α) y : α)),
    Prime (M := α) ((normalize : (a : α) → α) y : α)
⊢ Prime x

Tactic:
rcases Multiset.mem_map.1 hx with ⟨y, ⟨hy, rfl⟩⟩

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
y : α
hy : y ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯
hx :
  Membership.mem (α := α) (γ := Multiset α)
    (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
      (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
    ((normalize : (a : α) → α) y : α)
neg : Prime y
⊢ Prime (M := α) ((normalize : (a : α) → α) y : α)

Tactic:
rw [(normalize_associated _).prime_iff]

Premises used: Associated.prime_iff, normalize_associated
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
y : α
hy : y ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯
hx :
  Membership.mem (α := α) (γ := Multiset α)
    (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
      (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
    ((normalize : (a : α) → α) y : α)
⊢ Prime y

Tactic:
(Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 y hy

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Classical.choose_spec, And.left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
y : α
hy : y ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯
hx :
  Membership.mem (α := α) (γ := Multiset α)
    (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
      (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
    ((normalize : (a : α) → α) y : α)
⊢ Prime y

Tactic:
exact (Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 y hy

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Classical.choose_spec, And.left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ normalizedFactors a, Irreducible x

Tactic:
fun x h =>
  (prime_of_normalized_factor x h).irreducible

Premises used: Prime.irreducible, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
pos :
  ∀ (h : a = 0) (x : α),
    Membership.mem (γ := Multiset α) (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x) 0) x →
      (normalize : (a : α) → α) x = x
neg :
  ∀ (h : ¬a = 0) (x : α),
    Membership.mem (γ := Multiset α)
        (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
          (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
        x →
      (normalize : (a : α) → α) x = x
⊢ ∀ (x : α),
    Membership.mem (γ := Multiset α)
        (Multiset.map (α := α) (⇑normalize : (a : α) → α)
          (if h : a = 0 then 0 else Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
        x →
      (normalize : (a : α) → α) x = x

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ ∀ (x : α),
    Membership.mem (γ := Multiset α) (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x) 0) x →
      (normalize : (a : α) → α) x = x

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
x : α
hx :
  Membership.mem (γ := Multiset α)
    (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
      (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
    x
neg :
  ∀ y ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯,
    ∀
      (hx :
        Membership.mem (α := α) (γ := Multiset α)
          (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
            (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
          ((normalize : (a : α) → α) y : α)),
      Eq (α := α) ((normalize : (a : α) → α) ((normalize : (a : α) → α) y : α) : α) ((normalize : (a : α) → α) y : α)
⊢ (normalize : (a : α) → α) x = x

Tactic:
obtain ⟨y, _, rfl⟩ := Multiset.mem_map.1 hx

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
y : α
left : y ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯
hx :
  Membership.mem (α := α) (γ := Multiset α)
    (Multiset.map (fun (x : α) ↦ (normalize : (a : α) → α) x)
      (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯))
    ((normalize : (a : α) → α) y : α)
⊢ Eq (α := α) ((normalize : (a : α) → α) ((normalize : (a : α) → α) y : α) : α) ((normalize : (a : α) → α) y : α)

Tactic:
apply normalize_idem

Premises used: normalize_idem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
obtain :
  ∀ (p : α) (a_assoc : a ~ᵤ p) (hp : normalizedFactors a = {p}),
    normalizedFactors a = singleton (α := α) ((normalize : (a : α) → α) a : α)
⊢ normalizedFactors a = singleton (α := α) ((normalize : (a : α) → α) a : α)

Tactic:
obtain ⟨p, a_assoc, hp⟩ :=
    prime_factors_irreducible ha ⟨prime_of_normalized_factor, prod_normalizedFactors ha.ne_zero⟩

Premises used: prime_factors_irreducible, UniqueFactorizationMonoid.prime_of_normalized_factor, UniqueFactorizationMonoid.prod_normalizedFactors, And.intro, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
rw : Membership.mem (γ := Multiset α) {p} p
⊢ p ∈ normalizedFactors a

Tactic:
rw [hp]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ Membership.mem (γ := Multiset α) {p} p

Tactic:
Multiset.mem_singleton_self _

Premises used: Multiset.mem_singleton_self
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ Membership.mem (γ := Multiset α) {p} p

Tactic:
exact Multiset.mem_singleton_self _

Premises used: Multiset.mem_singleton_self
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ normalizedFactors a

Tactic:
have p_mem : p ∈ normalizedFactors a := by
    rw [hp]
    exact Multiset.mem_singleton_self _
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ normalizedFactors a = {p}

Tactic:
hp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
h : (normalize : (a : α) → α) a = p
⊢ normalizedFactors a = singleton (α := α) ((normalize : (a : α) → α) a : α)

Tactic:
convert! hp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
h : Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) p : α)
h₁ : a ∣ p ∧ p ∣ a
h₂ h₃ h₄ h₅ : a ~ᵤ p
⊢ (normalize : (a : α) → α) a = p

Tactic:
rwa [← normalize_normalized_factor p p_mem, normalize_eq_normalize_iff, dvd_dvd_iff_associated]

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor, normalize_eq_normalize_iff, dvd_dvd_iff_associated
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
normalize_eq_normalize hdvd
      ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
        (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
h : p = (normalize : (a : α) → α) p
h₁ : q = (normalize : (a : α) → α) q
⊢ p = q

Tactic:
convert!
    normalize_eq_normalize hdvd
      ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
        (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = (normalize : (a : α) → α) p

Tactic:
apply (normalize_normalized_factor _ ‹_›).symm

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor, Eq.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ q = (normalize : (a : α) → α) q

Tactic:
apply (normalize_normalized_factor _ ‹_›).symm

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor, Eq.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
rw : p * b ~ᵤ p * (normalizedFactors b).prod
⊢ p * b ~ᵤ (p ::ₘ normalizedFactors b).prod

Tactic:
rw [Multiset.prod_cons]

Premises used: Multiset.prod_cons
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (normalizedFactors b).prod

Tactic:
(prod_normalizedFactors hb0).symm.mul_left _

Premises used: Associated.symm, UniqueFactorizationMonoid.prod_normalizedFactors, Associated.mul_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (normalizedFactors b).prod

Tactic:
exact (prod_normalizedFactors hb0).symm.mul_left _

Premises used: Associated.symm, UniqueFactorizationMonoid.prod_normalizedFactors, Associated.mul_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
this : Multiset.Rel Associated (p ::ₘ normalizedFactors b) (normalizedFactors a)
⊢ p ∈ p ::ₘ normalizedFactors b

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
obtain : ∀ (p' : α) (hp' : Irreducible p') (hp'x : p' ∣ x), ∃ (p : α), p ∈ normalizedFactors x
⊢ ∃ (p : α), p ∈ normalizedFactors x

Tactic:
obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx

Premises used: WfDvdMonoid.exists_irreducible_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
obtain : ∀ (p : α) (hp : p ∈ normalizedFactors x), p' ~ᵤ p → ∃ (p : α), p ∈ normalizedFactors x
⊢ ∃ (p : α), p ∈ normalizedFactors x

Tactic:
obtain ⟨p, hp, _⟩ := exists_mem_normalizedFactors_of_dvd hx hp' hp'x

Premises used: UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ normalizedFactors x
right : p' ~ᵤ p
⊢ ∃ (p : α), p ∈ normalizedFactors x

Tactic:
⟨p, hp⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ normalizedFactors x
right : p' ~ᵤ p
⊢ ∃ (p : α), p ∈ normalizedFactors x

Tactic:
exact ⟨p, hp⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 0) 0

Tactic:
simp [normalizedFactors, factors]

Premises used: UniqueFactorizationMonoid.normalizedFactors, UniqueFactorizationMonoid.factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inl : ∀ (h : Subsingleton α), Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 1) 0
inr : ∀ (h : Nontrivial α), Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 1) 0
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 1) 0

Tactic:
rcases subsingleton_or_nontrivial α with h | h

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ Eq.{u_1 + 1} (α := Multiset α)
    (Multiset.map (α := α) (⇑normalize : (a : α) → α)
      (if h : Eq.{u_1 + 1} (α := α) 1 0 then 0
      else Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ 1) ⋯))
    0

Tactic:
simp [Subsingleton.elim (1 : α) 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
inr : Multiset.Rel.{u_1, u_1} (α := α) Associated (normalizedFactors 1) 0
rw : Type u_1
rw₁ : α → α → Prop
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 1) 0

Tactic:
rw [← Multiset.rel_zero_right]

Premises used: Multiset.rel_zero_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
x : α
hx : Membership.mem (γ := Multiset α) 0 x
inr : False
⊢ Irreducible x

Tactic:
exfalso