case h.h
F : Type ?u.90892
α✝ : Type ?u.90895
β✝ : Type ?u.90898
γ : Type ?u.90901
δ : Type ?u.90904
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
x✝ : α
⊢ ↑(ofRelIsoLT (toRelIsoLT e)) x✝ = ↑e x✝
F : Type ?u.90892
α✝ : Type ?u.90895
β✝ : Type ?u.90898
γ : Type ?u.90901
δ : Type ?u.90904
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
⊢ ofRelIsoLT (toRelIsoLT e) = e
ext
no goals
case h.h
F : Type ?u.90892
α✝ : Type ?u.90895
β✝ : Type ?u.90898
γ : Type ?u.90901
δ : Type ?u.90904
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
x✝ : α
⊢ ↑(ofRelIsoLT (toRelIsoLT e)) x✝ = ↑e x✝
simp