Overlap implies distance

lemma overlap_implies_distance (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₁ ∪ t u₂)    (hpu₁ : ¬Disjoint (𝓘 p : Set X) (𝓘 u₁)) : p ∈ 𝔖₀ t u₁ u₂ := by  simp_rw [𝔖₀, mem_setOf, hp, true_and]  wlog plu₁ : 𝓘 p ≤ 𝓘 u₁ generalizing p  · have u₁lp : 𝓘 u₁ ≤ 𝓘 p := (le_or_ge_or_disjoint.resolve_left plu₁).resolve_right hpu₁    obtain ⟨p', mp'⟩ := t.nonempty hu₁    have p'lu₁ : 𝓘 p' ≤ 𝓘 u₁ := (t.smul_four_le hu₁ mp').1    obtain ⟨c, mc⟩ := (𝓘 p').nonempty    specialize this (mem_union_left _ mp') (not_disjoint_iff.mpr ⟨c, mc, p'lu₁.1 mc⟩) p'lu₁    exact this.trans (Grid.dist_mono (p'lu₁.trans u₁lp))  have four_Z := four_le_Z (X := X)  have four_le_Zn : 4 ≤ Z * (n + 1) := by rw [← mul_one 4]; exact mul_le_mul' four_Z (by lia)  have four_le_two_pow_Zn : 4 ≤ 2 ^ (Z * (n + 1) - 1) := by    change 2 ^ 2 ≤ _; exact Nat.pow_le_pow_right zero_lt_two (by lia)  have ha : (2 : ℝ) ^ (Z * (n + 1)) - 4 ≥ 2 ^ (Z * n / 2 : ℝ) :=    calc      _ ≥ (2 : ℝ) ^ (Z * (n + 1)) - 2 ^ (Z * (n + 1) - 1) := by gcongr; norm_cast      _ = 2 ^ (Z * (n + 1) - 1) := by        rw [sub_eq_iff_eq_add, ← two_mul, ← pow_succ', Nat.sub_add_cancel (by lia)]      _ ≥ 2 ^ (Z * n) := by apply pow_le_pow_right₀ one_le_two; rw [mul_add_one]; lia      _ ≥ _ := by        rw [← Real.rpow_natCast]        apply Real.rpow_le_rpow_of_exponent_le one_le_two; rw [Nat.cast_mul]        exact half_le_self (by positivity)  rcases hp with (c : p ∈ t.𝔗 u₁) | (c : p ∈ t.𝔗 u₂)  · calc    _ ≥ dist_(p) (𝒬 p) (𝒬 u₂) - dist_(p) (𝒬 p) (𝒬 u₁) := by      change _ ≤ _; rw [sub_le_iff_le_add, add_comm]; exact dist_triangle ..    _ ≥ 2 ^ (Z * (n + 1)) - 4 := by      gcongr      · exact (t.lt_dist' hu₂ hu₁ hu.symm c (plu₁.trans h2u)).le      · have : 𝒬 u₁ ∈ ball_(p) (𝒬 p) 4 :=          (t.smul_four_le hu₁ c).2 (by convert! mem_ball_self zero_lt_one)        exact (@mem_ball' _ (instPseudoMetricSpaceWithFunctionDistance (x := 𝔠 p) (r := ↑D ^ 𝔰 p / 4)) _ _ _).mp this |>.le    _ ≥ _ := ha  · calc    _ ≥ dist_(p) (𝒬 p) (𝒬 u₁) - dist_(p) (𝒬 p) (𝒬 u₂) := by      change _ ≤ _; rw [sub_le_iff_le_add, add_comm]; exact dist_triangle_right ..    _ ≥ 2 ^ (Z * (n + 1)) - 4 := by      gcongr      · exact (t.lt_dist' hu₁ hu₂ hu c plu₁).le      · have : 𝒬 u₂ ∈ ball_(p) (𝒬 p) 4 :=          (t.smul_four_le hu₂ c).2 (by convert! mem_ball_self zero_lt_one)        exact (@mem_ball' _ (instPseudoMetricSpaceWithFunctionDistance (x := 𝔠 p) (r := ↑D ^ 𝔰 p / 4)) _ _ _).mp this |>.le    _ ≥ _ := ha