Grid.isMin_iff

lemma isMin_iff {i : Grid X} : IsMin i ↔ s i = - S := by  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩  · apply le_antisymm ?_ scale_mem_Icc.1    contrapose! h    have : -(S : ℤ) ∈ Ico (-(S : ℤ)) (s i) := by simp [h]    have := Grid_subset_biUnion (i := i) (-S) this c_mem_Grid    push _ ∈ _ at this    rcases this with ⟨j, (hj : s j = -(S : ℤ)), h'j⟩    have sji : s j < s i := by simpa [hj] using h    have : (j : Set X) ⊆ i := by      rcases fundamental_dyadic sji.le with hji | h_disj      · exact hji      · exact (disjoint_right.1 h_disj c_mem_Grid h'j).elim    have : j < i := by simp [this, sji]    exact this.not_isMin  · intro j hj    have : s i ≤ s j := by rw [h]; exact (scale_mem_Icc (i := j)).1    rcases le_or_disjoint this with h' | h_disj    · exact h'    · exact False.elim (disjoint_right.1 h_disj c_mem_Grid (hj.1 c_mem_Grid))