case h.h.mk
F : Type ?u.52049
α : Type u_1
β : Type u_2
γ : Type ?u.52058
δ : Type ?u.52061
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
x : α
y : β
⊢ ↑(OrderHom.prod fst snd) (x, y) = ↑id (x, y)
F : Type ?u.52049
α : Type u_1
β : Type u_2
γ : Type ?u.52058
δ : Type ?u.52061
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
⊢ OrderHom.prod fst snd = id
ext ⟨x, y⟩ : 2
no goals
case h.h.mk
F : Type ?u.52049
α : Type u_1
β : Type u_2
γ : Type ?u.52058
δ : Type ?u.52061
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
x : α
y : β
⊢ ↑(OrderHom.prod fst snd) (x, y) = ↑id (x, y)
rfl