case h.h
F : Type ?u.47398
α : Type u_1
β : Type u_2
γ : Type ?u.47407
δ : Type ?u.47410
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α →o β
x✝ : α
⊢ ↑(comp f id) x✝ = ↑f x✝
F : Type ?u.47398
α : Type u_1
β : Type u_2
γ : Type ?u.47407
δ : Type ?u.47410
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α →o β
⊢ comp f id = f
ext
no goals
case h.h
F : Type ?u.47398
α : Type u_1
β : Type u_2
γ : Type ?u.47407
δ : Type ?u.47410
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α →o β
x✝ : α
⊢ ↑(comp f id) x✝ = ↑f x✝
rfl