Theorem: PreHFSet.rank_eq_zero_iff (Hfzfa.lean)

State before:
atoms : Type u_1
a✝ : atoms
⊢ rank (atom a✝) = 0 ↔ isAtom (atom a✝) = true
Tactic:
simp [rank, isAtom]
State after:
no goals

State before:
atoms : Type u_1
n✝ : ℕ
a✝ : Fin n✝ → PreHFSet atoms
⊢ rank (lst a✝) = 0 ↔ isAtom (lst a✝) = true
Tactic:
simp [rank, isAtom]
State after:
no goals