transitive_boundary'

lemma transitive_boundary' {k1 k2 k3 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2) (hk3 : -S ≤ k3)  (hk1_2 : k1 < k2) (hk2_3 : k2 ≤ k3) (y1 : Yk X k1) (y2 : Yk X k2) (y3 : Yk X k3)    (x : X) (hx : x ∈ I3 hk1 y1 ∩ I3 hk2 y2 ∩ I3 hk3 y3) :    clProp(hk1,y1|hk3,y3) → (clProp(hk1,y1|hk2,y2) ∧ clProp(hk2,y2|hk3,y3)) := by  rintro ⟨_, hx'⟩  have hi3_1_2 : I3 hk1 y1 ⊆ I3 hk2 y2 := by    apply dyadic_property hk1 hk1_2.le hk2 y2 y1    rw [not_disjoint_iff]    exact ⟨x, hx.left.left, hx.left.right⟩  have hi3_2_3 : I3 hk2 y2 ⊆ I3 hk3 y3 := by    apply dyadic_property hk2 hk2_3 hk3 y3 y2    rw [not_disjoint_iff]    exact ⟨x, hx.left.right, hx.right⟩  have hx_4k2 : x ∈ ball (y2 : X) (4 * D ^ k2) := I3_prop_3_2 hk2 y2 hx.left.right  have hx_4k2' : x ∈ ball (y1 : X) (4 * D ^ k1) := I3_prop_3_2 hk1 y1 hx.left.left  have hd_nzero : (D : ℝ≥0∞) ≠ 0 := by    apply LT.lt.ne'    rw [← ENNReal.ofReal_natCast, ENNReal.ofReal_pos]    exact realD_pos a  have hdp_nzero : ∀ (z:ℤ),(D ^ z :ℝ≥0∞) ≠ 0 := by    intro z    exact (ENNReal.zpow_pos hd_nzero (by finiteness) _).ne'  have hdp_finit42 : (D ^ 42 : ℝ≥0∞) ≠ ⊤ := by finiteness  refine ⟨⟨hi3_1_2, ?_⟩, ⟨hi3_2_3, ?_⟩⟩  · apply lt_of_le_of_lt (Metric.infEDist_anti _) hx'    rw [compl_subset_compl]    exact hi3_2_3  · rw [← eball_ofReal, Metric.mem_eball] at hx_4k2 hx_4k2'    rw [edist_comm] at hx_4k2'    rw [← Real.rpow_intCast] at hx_4k2 hx_4k2'    rw [ENNReal.ofReal_mul (by norm_num), ← ENNReal.ofReal_rpow_of_pos (realD_pos a),      ENNReal.ofReal_ofNat,ENNReal.ofReal_natCast,ENNReal.rpow_intCast] at hx_4k2 hx_4k2'    calc      Metric.infEDist (y2 : X) (I3 hk3 y3)ᶜ        ≤ edist (y2 : X) (y1 : X) + Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ :=          Metric.infEDist_le_edist_add_infEDist      _ = Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ + edist (y1 : X) (y2 : X) := by        rw [add_comm,edist_comm]      _ ≤ Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ +          (edist (y1:X) x + edist x y2) := by        rw [ENNReal.add_le_add_iff_left hx'.ne_top]        exact edist_triangle (↑y1) x ↑y2      _ < Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ + edist (y1 : X) x + 4 * D ^ k2 := by        rw [← add_assoc, ENNReal.add_lt_add_iff_left (by finiteness)]        exact hx_4k2      _ < 6 * D ^ k1 + 4 * D ^ k1 + 4 * D ^ k2 := by        rw [ENNReal.add_lt_add_iff_right]        · apply ENNReal.add_lt_add hx' hx_4k2'        · finiteness      _ ≤ 2 * D ^ k2 + 4 * D ^ k2 := by        rw [← right_distrib 6 4 (D ^ k1 : ℝ≥0∞)]        have hz : (6 + 4 : ℝ≥0∞) = 2 * 5 := by norm_num        rw [hz, ENNReal.add_le_add_iff_right, mul_assoc]        · gcongr          calc            (5 * D ^ k1 : ℝ≥0∞)              ≤ D * D ^ k1 := by                gcongr                rw [← ENNReal.ofReal_ofNat,← ENNReal.ofReal_natCast,                  ENNReal.ofReal_le_ofReal_iff <| realD_nonneg a]                exact five_le_realD X            _ ≤ D ^ k2 := by              nth_rw 1 [← zpow_one (D : ℝ≥0∞)]              simp_rw [← ENNReal.rpow_intCast]              rw [← ENNReal.rpow_add _ _ hd_nzero (by finiteness),← Int.cast_add]              apply ENNReal.rpow_le_rpow_of_exponent_le              · rw [← ENNReal.ofReal_one,← ENNReal.ofReal_natCast]                rw [ENNReal.ofReal_le_ofReal_iff <| realD_nonneg a]                exact one_le_realD a              simp only [Int.cast_le]              linarith        · finiteness      _ = 6 * D ^ k2 := by        rw [← right_distrib]        norm_num