no goals
α : Type u_1
β : Type u_2
γ : Type ?u.83181
δ : Type ?u.83184
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
x : β
y : α
⊢ r (↑(RelIso.symm e) x) y ↔ s x (↑e y)
rw [← e.map_rel_iff, e.apply_symm_apply]