TileStructure.Forest.subset_of_kissing

lemma subset_of_kissing (h : J ∈ kissing I) :    ball (c J) (D ^ s J / 4) ⊆ ball (c I) (33 * D ^ s I) := by  simp_rw [kissing, Finset.mem_filter_univ] at h  obtain ⟨x, xI, xJ⟩ := not_disjoint_iff.mp h.2  apply ball_subset_ball'  calc    _ ≤ D ^ s J / 4 + dist (c J) x + dist x (c I) := by      rw [add_assoc]; exact add_le_add_right (dist_triangle ..) _    _ ≤ D ^ s J / 4 + 16 * D ^ s J + 16 * D ^ s I := by      gcongr      · exact (mem_ball'.mp xJ).le      · exact (mem_ball.mp xI).le    _ ≤ _ := by      rw [h.1, div_eq_mul_inv, mul_comm _ 4⁻¹, ← distrib_three_right]      gcongr      norm_num