TileStructure.Forest.convex_scales

lemma convex_scales (hu : u ∈ t) : OrdConnected (t.σ u x : Set ℤ) := by  rw [ordConnected_def]; intro i mi j mj k mk  simp_rw [Finset.mem_coe, σ, Finset.mem_image, Finset.mem_filter, Finset.mem_univ,    true_and] at mi mj ⊢  obtain ⟨p, ⟨mp, xp, Qxp, sxp⟩, sp⟩ := mi  obtain ⟨p'', ⟨mp'', xp'', Qxp'', sxp''⟩, sp''⟩ := mj  have ilj : i ≤ j := nonempty_Icc.mp ⟨k, mk⟩  rw [← sp, ← sp''] at ilj mk  obtain ⟨K, sK, lK, Kl⟩ := Grid.exists_sandwiched (le_of_mem_of_mem ilj xp xp'') k mk  have := range_subset_iff.mp (biUnion_Ω (i := K)) x  simp_rw [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop] at this  obtain ⟨(p' : 𝔓 X), (𝓘p' : 𝓘 p' = K), Qxp'⟩ := this  rw [← 𝓘p'] at lK Kl sK; refine ⟨p', ?_, sK⟩  have l₁ : p ≤ p' := tile_le_of_cube_le_and_not_disjoint lK Qxp Qxp'  have l₂ : p' ≤ p'' := tile_le_of_cube_le_and_not_disjoint Kl Qxp' Qxp''  refine ⟨(t.ordConnected hu).out mp mp'' ⟨l₁, l₂⟩, ⟨(Grid.le_def.mp lK).1 xp, Qxp', ?_⟩⟩  exact Icc_subset_Icc sxp.1 sxp''.2 ⟨(Grid.le_def.mp lK).2, (Grid.le_def.mp Kl).2⟩