Theorem: HFSet.mem_ofMultiset_iff (Hfzfa.lean)

State before:
atoms : Type u_1
s : Multiset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ ofMultiset 0 ↔ x ∈ 0
Tactic:
simp [ofMultiset]
State after:
no goals

State before:
atoms : Type u_1
s✝ : Multiset (HFSet atoms)
x y : HFSet atoms
s : Multiset (HFSet atoms)
ih : x ∈ ofMultiset s ↔ x ∈ s
⊢ x ∈ ofMultiset (y ::ₘ s) ↔ x ∈ y ::ₘ s
Tactic:
simp [ih]
State after:
no goals