α : Type u_1
inst✝ : CommMonoidWithZero α
h : WfDvdMonoid (Associates α)
⊢ ∀ {a b : α}, DvdNotUnit a b ↔ DvdNotUnit (Associates.mk a) (Associates.mk b)
α : Type u_1
inst✝ : CommMonoidWithZero α
h : WfDvdMonoid (Associates α)
⊢ WellFounded DvdNotUnit
refine' (Surjective.wellFounded_iff mk_surjective _).2 wellFounded_dvdNotUnit
α : Type u_1
inst✝ : CommMonoidWithZero α
h : WfDvdMonoid (Associates α)
a✝ b✝ : α
⊢ DvdNotUnit a✝ b✝ ↔ DvdNotUnit (Associates.mk a✝) (Associates.mk b✝)
α : Type u_1
inst✝ : CommMonoidWithZero α
h : WfDvdMonoid (Associates α)
⊢ ∀ {a b : α}, DvdNotUnit a b ↔ DvdNotUnit (Associates.mk a) (Associates.mk b)
intros
no goals
α : Type u_1
inst✝ : CommMonoidWithZero α
h : WfDvdMonoid (Associates α)
a✝ b✝ : α
⊢ DvdNotUnit a✝ b✝ ↔ DvdNotUnit (Associates.mk a✝) (Associates.mk b✝)
rw [mk_dvdNotUnit_mk_iff]