no goals
ι✝ : Type ?u.46874
α✝ : Type u
β : Type v
γ : Type w
π : ι✝ → Type ?u.46885
r : α✝ → α✝ → Prop
ι : Type u
α : ι → Type v
inst✝ : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
⊢ x < y ↔ x ≤ y ∧ ∃ i, x i < y i
simp (config := { contextual := true }) [lt_iff_le_not_le, Pi.le_def]