Grid.exists_supercube

lemma exists_supercube (l : ℤ) (h : l ∈ Icc (s i) S) : ∃ j, s j = l ∧ i ≤ j := by  obtain ⟨lb, ub⟩ := h  rcases ub.eq_or_lt with ub | ub; · exact ⟨topCube, by simpa [ub] using! s_topCube, le_topCube⟩  obtain ⟨x, hx⟩ := i.nonempty  have bound_i : -S ≤ s i ∧ s i ≤ S := scale_mem_Icc  have ts := Grid_subset_biUnion (X := X) (i := topCube) l    (by rw [s_topCube, mem_Ico]; omega)  have := mem_of_mem_of_subset hx ((le_topCube (i := i)).1.trans ts)  push _ ∈ _ at this  obtain ⟨j, (sj : s j = l), mj⟩ := this; use j, sj  exact le_of_mem_of_mem (by lia) hx mj