Theorem: LoVe.mem_restrict (LoVe/LoVelib.lean)

State before:
α : Type
r : Set (α × α)
P : α → Prop
a b : α
⊢ (a, b) ∈ r ⇃ P ↔ (a, b) ∈ r ∧ P a
Tactic:
rfl
State after:
no goals