no goals
ι : Type ?u.73668
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.73679
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b
simpa [Pi.lt_def] using le_of_lt