α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ factors a
ha : a = 0
⊢ False
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ factors a
⊢ a ≠ 0
intro ha
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ 0
ha : a = 0
⊢ False
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ factors a
ha : a = 0
⊢ False
rw [factors, dif_pos ha] at h
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ 0
ha : a = 0
⊢ False
exact Multiset.not_mem_zero _ h