Construction.Ω_subset_cball

lemma Ω_subset_cball {p : 𝔓 X} : Ω p ⊆ ball_(p) (𝒬 p) 1 := by  induction p using 𝔓_induction with  | base p maxI =>    rw [Ω]; simp only [maxI, dite_true]    exact (Ω₁_subset_ball p).trans (ball_subset_ball (by norm_num))  | ind p nmaxI ih =>    rw [Ω]; simp only [nmaxI, dite_false]    intro ϑ mϑ    rcases mϑ with c | c; · exact mem_of_mem_of_subset c (ball_subset_ball (by norm_num))    obtain ⟨I, ⟨y, my⟩⟩ := p    dsimp only at nmaxI ih c    set J := I.succ    rw [mem_iUnion₂] at c    obtain ⟨z, ⟨mz₁, mz₂⟩, hz⟩ := c    simp only [mem_ball]    calc      _ ≤ dist_{I} ϑ z + dist_{I} z y := dist_triangle ..      _ < dist_{I} ϑ z + C4_2_1 := by        gcongr; simpa using! (Ω₁_subset_ball ⟨I, ⟨y, my⟩⟩) mz₂      _ ≤ C2_1_2 a * dist_{J} ϑ z + C4_2_1 := by        gcongr; refine Grid.dist_strictMono (lt_of_le_of_ne Grid.le_succ ?_)        contrapose! nmaxI; exact Grid.max_of_le_succ nmaxI.symm.le      _ < C2_1_2 a * 1 + C4_2_1 := by        gcongr        · rw [C2_1_2]; positivity        · simpa only [mem_ball] using! (ih ⟨z, mz₁⟩) hz      _ < 2 ^ (-2 : ℝ) + C4_2_1 := by        gcongr        rw [mul_one, C2_1_2, Real.rpow_lt_rpow_left_iff one_lt_two, lt_neg]        simp only [add_mul, neg_mul, neg_add_rev, neg_neg, lt_neg_add_iff_add_lt]        norm_cast        calc        5 * a + 2        _ < 6 * a := by linarith [four_le_a X]        _ ≤ 𝕔 * a := by          gcongr          linarith [seven_le_c]      _ < _ := by norm_num