case h
F : Type ?u.91547
α✝ : Type ?u.91550
β✝ : Type ?u.91553
γ : Type ?u.91556
δ : Type ?u.91559
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1
x✝ : α
⊢ ↑(toRelIsoLT (ofRelIsoLT e)) x✝ = ↑e x✝
F : Type ?u.91547
α✝ : Type ?u.91550
β✝ : Type ?u.91553
γ : Type ?u.91556
δ : Type ?u.91559
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1
⊢ toRelIsoLT (ofRelIsoLT e) = e
ext
no goals
case h
F : Type ?u.91547
α✝ : Type ?u.91550
β✝ : Type ?u.91553
γ : Type ?u.91556
δ : Type ?u.91559
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1
x✝ : α
⊢ ↑(toRelIsoLT (ofRelIsoLT e)) x✝ = ↑e x✝
simp