no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
q : (j : Fin (n + 1)) → α j
⊢ insertNth i x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j => q (↑(succAbove i) j)
simp [Pi.le_def, forall_iff_succAbove i]