case h.h'.h.e'_2.h.h.e'_1.h.h'.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
⊢ ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
convert eif using 7
no goals
case h.h'.h.e'_2.h.h.e'_1.h.h'.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹
simp_rw [irreducible_iff_prime_of_exists_unique_irreducible_factors eif uif]