Theorem: HFSet.ofMultiset_isAtom (Hfzfa.lean)

State before:
atoms : Type u_1
s : Multiset (HFSet atoms)
⊢ isAtom (ofMultiset 0) = false
Tactic:
simp [ofMultiset]
State after:
no goals

State before:
atoms : Type u_1
s✝ : Multiset (HFSet atoms)
y : HFSet atoms
s : Multiset (HFSet atoms)
ih : isAtom (ofMultiset s) = false
⊢ isAtom (ofMultiset (y ::ₘ s)) = false
Tactic:
simpa
State after:
no goals