no goals
𝕜 : Type ?u.1103
ι : Type ?u.1106
κ : Type ?u.1109
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
x : α × β
⊢ x ∈ interedges r s t ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ r x.fst x.snd
rw [interedges, mem_filter, Finset.mem_product, and_assoc]