no goals
α✝ : Type ?u.30166
β✝ : Type ?u.30169
γ : Type ?u.30172
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : β ≃ α
⊢ (type fun x y => r (↑f x) (↑f y)) = type r
convert (RelIso.preimage f r).ordinal_type_eq