Theorem: Partial.empty_iff_ids_empty (ReactorModel/Extensions.lean)

State before:
α : Type u_1
β : Type u_2
f : α ⇀ β
⊢ f = ∅ ↔ ids f = ∅
Tactic:
simp [ids, empty_iff, Set.eq_empty_iff_forall_not_mem, Option.eq_none_iff_forall_not_mem]
State after:
no goals