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

State before:
α : Type u_1
β : Type u_2
a : α
f : α ⇀ β
⊢ a ∈ f ↔ ∃ b, f a = some b
Tactic:
rfl
State after:
no goals