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

State before:
α : Type
r₁ r₂ : Set (α × α)
a b : α
⊢ (a, b) ∈ r₁ ◯ r₂ ↔ ∃ c, (a, c) ∈ r₁ ∧ (c, b) ∈ r₂
Tactic:
rfl
State after:
no goals