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