case h.h.a
α : Type u_1
β : Type u_2
γ : Type ?u.37384
δ : Type ?u.37387
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (↑f ⁻¹'o s) a b
α : Type u_1
β : Type u_2
γ : Type ?u.37384
δ : Type ?u.37387
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
⊢ r = ↑f ⁻¹'o s
ext (a b)
no goals
case h.h.a
α : Type u_1
β : Type u_2
γ : Type ?u.37384
δ : Type ?u.37387
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (↑f ⁻¹'o s) a b
exact f.map_rel_iff.symm