R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R),
      (b ∈
          if h : a = 0 then ∅
          else choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a)) →
        Irreducible b) ∧
    Associated
      (Multiset.prod
        (if h : a = 0 then ∅
        else choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a)))
      a
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R), b ∈ factors a → Irreducible b) ∧ Associated (Multiset.prod (factors a)) a
unfold factors
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R),
      b ∈ choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a) → Irreducible b) ∧
    Associated (Multiset.prod (choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a))) a
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R),
      (b ∈
          if h : a = 0 then ∅
          else choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a)) →
        Irreducible b) ∧
    Associated
      (Multiset.prod
        (if h : a = 0 then ∅
        else choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a)))
      a
rw [dif_neg h]
no goals
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R),
      b ∈ choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a) → Irreducible b) ∧
    Associated (Multiset.prod (choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a))) a
exact Classical.choose_spec (WfDvdMonoid.exists_factors a h)