no goals
α : Type u
β : Type v
ι : Type ?u.169884
π : ι → Type ?u.169889
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
K : CompactExhaustion α
x : α
⊢ ¬CompactExhaustion.find (shiftr K) x ≤ CompactExhaustion.find K x
simp only [find_shiftr, not_le, Nat.lt_succ_self]