I3_prop_3_1

lemma I3_prop_3_1 {k : ℤ} (hk : -S ≤ k) (y : Yk X k) :    ball (y : X) (2⁻¹ * D ^ k) ⊆ I3 hk y := by  rw [I3, I1]  apply subset_trans _ subset_union_left  by_cases hk_s : k = -S  · rw [dif_pos hk_s]    subst hk_s    apply ball_subset_ball    nth_rw 2 [← one_mul (D ^ (-S : ℤ) : ℝ)]    gcongr; norm_num  · rw [dif_neg hk_s]    simp only [mem_preimage]    have : (y : X) ∈ ball o (4 * D ^ S - D ^ k : ℝ) := Yk_subset k y.property    have : ball (y : X) (2⁻¹ * D ^ k) ⊆ ⋃ (y' : Yk X (k - 1)), I3 (I_induction_proof hk hk_s) y' := by      calc        ball (y : X) (2⁻¹ * D ^ k)          ⊆ ball o (4 * D ^ S - D ^ k + 2⁻¹ * D ^ k) := by            apply ball_subset            ring_nf            rw [mul_comm]            rw [mem_ball] at this            exact this.le        _ ⊆ ball o (4 * D ^ S - 2 * D ^ (k - 1)) := by          apply ball_subset_ball          rw [sub_eq_add_neg,sub_eq_add_neg, add_assoc, add_le_add_iff_left]          simp only [neg_add_le_iff_le_add, le_add_neg_iff_add_le]          calc            (2⁻¹ * D ^ k + 2 * D ^ (k - 1) : ℝ)              = 2⁻¹ * D ^ k + 2⁻¹ * 4 * D ^ (k - 1) := by                rw [add_right_inj]                norm_num            _ ≤ 2⁻¹ * (2 * D ^ k) := by              rw [mul_assoc, ← left_distrib, two_mul]              gcongr              nth_rw 2 [← add_sub_cancel 1 k]              rw [zpow_add₀ (realD_pos a).ne.symm, zpow_one]              gcongr; exact four_le_realD X            _ = D ^ k := by              rw [← mul_assoc]              norm_num        _ ⊆ ⋃ (y' : Yk X (k - 1)), I3 (I_induction_proof hk hk_s) y' := I3_prop_2 (I_induction_proof hk hk_s)    intro x hx    have : x ∈ ⋃ (y' : Yk X (k - 1)), I3 _ y' := this hx    rw [mem_iUnion] at this    obtain ⟨y',hy'⟩ := this    have : x ∈ ball (y' : X) (4 * D ^ (k - 1)) := I3_prop_3_2 _ y' hy'    have : (y' : X) ∈ ball (y : X) (D ^ k) := by      rw [mem_ball] at this hx ⊢      rw [dist_comm] at this      calc        dist (y' : X) (y : X)          ≤ dist (y' : X) x + dist x (y : X) := dist_triangle _ _ _        _ < 4 * D ^ (k - 1) + 2⁻¹ * D ^ k := add_lt_add this hx        _ = 2⁻¹ * 8 * D ^ (k - 1) + 2⁻¹ * D ^ k := by norm_num        _ ≤ 2⁻¹ * (D ^ k + D ^ k) := by          rw [mul_assoc, ← left_distrib]          gcongr          nth_rw 2 [← add_sub_cancel 1 k,]          rw [zpow_add₀ (realD_pos a).ne.symm,zpow_one]          gcongr          exact eight_le_realD X        _ = D ^ k := by ring    rw [mem_iUnion]    use y'    rw [mem_iUnion]    use this