𝕜 : Type ?u.102463
ι : Type ?u.102466
κ : Type ?u.102469
α : Type u_1
β : Type ?u.102475
r : α → α → Prop
inst✝ : DecidableRel r
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
hr : Symmetric r
x : α × α
⊢ (Prod.swap x).fst ∈ s ∧ (Prod.swap x).snd ∈ t ∧ r (Prod.swap x).snd (Prod.swap x).fst ↔
    x.fst ∈ t ∧ x.snd ∈ s ∧ r x.fst x.snd
𝕜 : Type ?u.102463
ι : Type ?u.102466
κ : Type ?u.102469
α : Type u_1
β : Type ?u.102475
r : α → α → Prop
inst✝ : DecidableRel r
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
hr : Symmetric r
x : α × α
⊢ Prod.swap x ∈ interedges r s t ↔ x ∈ interedges r t s
rw [mem_interedges_iff, mem_interedges_iff, hr.iff]
no goals
𝕜 : Type ?u.102463
ι : Type ?u.102466
κ : Type ?u.102469
α : Type u_1
β : Type ?u.102475
r : α → α → Prop
inst✝ : DecidableRel r
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
hr : Symmetric r
x : α × α
⊢ (Prod.swap x).fst ∈ s ∧ (Prod.swap x).snd ∈ t ∧ r (Prod.swap x).snd (Prod.swap x).fst ↔
    x.fst ∈ t ∧ x.snd ∈ s ∧ r x.fst x.snd
exact and_left_comm