Theorem: Partial.Nonempty.iff_ids_nonempty (ReactorModel/Extensions.lean)

State before:
α : Type u_1
β : Type u_2
f : α ⇀ β
⊢ Nonempty f ↔ Set.Nonempty (ids f)
Tactic:
simp [Nonempty, Set.nonempty_iff_ne_empty, empty_iff_ids_empty]
State after:
no goals