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

State before:
α : Type u_1
β : Type u_2
a : α
f : α ⇀ β
⊢ a ∈ f ↔ a ∈ ids f
Tactic:
rfl
State after:
no goals