case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) } ∈ factors' a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) } ∈ factors' a
obtain ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd ha0 hp hd
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ a_1 h,
    { val := Associates.mk a_1, property := (_ : Irreducible (Associates.mk a_1)) } =
      { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) }
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) } ∈ factors' a
apply Multiset.mem_pmap.mpr
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ h,
    { val := Associates.mk q, property := (_ : Irreducible (Associates.mk q)) } =
      { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) }
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ a_1 h,
    { val := Associates.mk a_1, property := (_ : Irreducible (Associates.mk a_1)) } =
      { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) }
use q
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ { val := Associates.mk q, property := (_ : Irreducible (Associates.mk q)) } =
    { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) }
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ h,
    { val := Associates.mk q, property := (_ : Irreducible (Associates.mk q)) } =
      { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) }
use hq
no goals
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ { val := Associates.mk q, property := (_ : Irreducible (Associates.mk q)) } =
    { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) }
exact Subtype.eq (Eq.symm (mk_eq_mk_iff_associated.mpr hpq))