I2_prop_2

lemma I2_prop_2 {k : ℤ} (hk : -S ≤ k) :      ball o (4 * D ^ S - 2 * D ^ k) ⊆ ⋃ (y : Yk X k), I2 hk y := by    simp only [I2, mem_preimage, iUnion_coe_set]    by_cases hk_s : k = -S    · simp_rw [dif_pos hk_s]      subst hk_s      calc        ball o (4 * D ^ S - 2 * (D ^ (-S : ℤ)))          ⊆ ball o (4 * D ^ S - D ^ (-S : ℤ)) := by            apply ball_subset_ball            rw [two_mul,tsub_le_iff_right,sub_add_add_cancel,le_add_iff_nonneg_right]            positivity        _ ⊆ ⋃ (i ∈ Yk X (-S)), ball i (2 * D ^ (-S : ℤ)) := cover_big_ball (-S : ℤ)    · simp_rw [dif_neg hk_s]      intro x hx      have : -S < k := lt_of_le_of_ne hk fun a_1 ↦ hk_s (id a_1.symm)      have : ((2 * (S + (k - 1))).toNat : ℤ) + 1 < 2 * (S + k) := by        rw [Int.toNat_of_nonneg (by linarith)]        linarith      have hsub1 : ball o (4 * D ^ S - 2 * D ^ k) ⊆ ⋃ y, I3 (I_induction_proof hk hk_s) y := by        calc          ball o (4 * D ^ S - 2 * D ^ k)            ⊆ ball o (4 * D ^ S - 2 * D ^ (k - 1)) := by              apply ball_subset_ball              simp only [tsub_le_iff_right]              rw [sub_eq_add_neg,add_assoc]              simp only [le_add_iff_nonneg_right, le_neg_add_iff_add_le, add_zero, Nat.ofNat_pos,                mul_le_mul_iff_right₀]              gcongr              exacts [one_le_realD a, by linarith]          _ ⊆ ⋃ y, I3 _ y := I3_prop_2 _      have hmem_i3 : x ∈ ⋃ y, I3 _ y := hsub1 hx      simp only [mem_iUnion] at hmem_i3      obtain ⟨y', hy''⟩ := hmem_i3      have hy''' : x ∈ ball (y' : X) (D ^ k) := by        apply (?_ : I3 _ y' ⊆ ball (y' : X) (D ^ k)) hy''        calc          I3 _ y'            ⊆ ball y' (4 * D ^ (k - 1)) := I3_prop_3_2 _ y'          _ ⊆ ball y' (D * D ^ (k - 1)) :=              ball_subset_ball (by gcongr; exact (four_le_realD X))          _ = ball (y': X) (D ^ k) := by            nth_rw 1 [← zpow_one (D : ℝ),← zpow_add₀ (realD_pos a).ne.symm, add_sub_cancel]      rw [mem_ball_comm] at hy'''      have hyfin : (y' : X) ∈ ball o (4 * D ^ S - D ^ k) := by        simp only [mem_ball] at hx hy''' ⊢        calc          dist ↑y' o            ≤ dist (y' : X) x + dist x o := dist_triangle _ _ _          _ < D ^ k + (4 * D ^ S - 2 * D ^ k) := add_lt_add hy''' hx          _ ≤ 4 * D ^ S - D ^ k := by linarith      have hyfin' : (y' : X) ∈ ⋃ (y'' ∈ Yk X k), ball (y'') (2 * D ^ k) := cover_big_ball k hyfin      rw [← iUnion_coe_set (Yk X k) (fun z ↦ ball (z : X) (2 * D ^ k))] at hyfin'      simp only [mem_iUnion] at hyfin'      obtain ⟨y2,hy2'⟩ := hyfin'      simp only [mem_iUnion, exists_prop, exists_and_left]      use y2, y2.property, y', hy2', y'.property