ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
inhabited_h : Inhabited ι
⊢ a < b
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
⊢ a < b
inhabit ι
no goals
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
inhabited_h : Inhabited ι
⊢ a < b
exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩