α : Type u_1
β : Type ?u.26091
γ : Type ?u.26094
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
α : Type u_1
β : Type ?u.26091
γ : Type ?u.26094
a b : α
m : Multiset α
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0
rw [← cons_zero, cons_eq_cons]
no goals
α : Type u_1
β : Type ?u.26091
γ : Type ?u.26094
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
simp [eq_comm]