exists_Grid

lemma exists_Grid {x : X} (hx : x ∈ G) {s : ℤ} (hs : s ∈ (Icc (σ₁ x) (σ₂ x)).toFinset) :    ∃ I : Grid X, GridStructure.s I = s ∧ x ∈ I := by  have DS : (D : ℝ) ^ S = (D : ℝ) ^ (S : ℤ) := rfl  have : x ∈ ball o (D ^ S / 4) := G_subset hx  rw [← c_topCube (X := X), DS, ← s_topCube (X := X)] at this  have x_mem_topCube := ball_subset_Grid this  by_cases hS : s = S -- Handle separately b/c `Grid_subset_biUnion`, as stated, doesn't cover `s=S`  · exact ⟨topCube, by rw [s_topCube, hS], x_mem_topCube⟩  have s_mem : s ∈ Ico (-S : ℤ) (GridStructure.s (X := X) topCube) :=    have : s ∈ Icc (-S : ℤ) S := Icc_σ_subset_Icc_S (mem_toFinset.1 hs)    ⟨this.1, s_topCube (X := X) ▸ lt_of_le_of_ne this.2 hS⟩  simpa only [mem_iUnion, exists_prop] using! Grid_subset_biUnion s s_mem x_mem_topCube