Theorem: HFSet.rank_ofFinset (Hfzfa.lean)

State before:
atoms : Type u_1
s : Finset (HFSet atoms)
⊢ rank (ofFinset s) = Finset.sup s rank + 1
Tactic:
classical
rw [rank_def] <;> simp
State after:
no goals

State before:
atoms : Type u_1
s : Finset (HFSet atoms)
⊢ rank (ofFinset s) = Finset.sup s rank + 1
Tactic:
rw [rank_def] <;> simp
State after:
no goals