no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : ¬x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (↑(succAbove i) j)
⊢ p ∈ insertNth i x ⁻¹' Icc q₁ q₂ ↔ p ∈ ∅
simp only [mem_preimage, insertNth_mem_Icc, hx, false_and_iff, mem_empty_iff_false]