I3_prop_3_2

lemma I3_prop_3_2 {k : ℤ} (hk : -S ≤ k) (y : Yk X k) :    I3 hk y ⊆ ball (y : X) (4 * D ^ k) := by  intro x hx  have : x ∈ I2 hk y := I3_subset_I2 hk y hx  simp only [I2] at this  by_cases hk_s : k = -S  · rw [dif_pos hk_s] at this    subst hk_s    revert this    apply ball_subset_ball (by gcongr; norm_num)  · rw [dif_neg hk_s] at this    push _ ∈ _ at this    obtain ⟨y',hy',hyi3⟩ := this    have : -S ≤ k - 1 := I_induction_proof hk hk_s    have : x ∈ ball (y' : X) (4 * D ^ (k-1)) := I3_prop_3_2 _ y' hyi3    rw [mem_ball] at this hy' ⊢    calc      dist x (y:X)        ≤ dist x (y' : X) + dist (y' : X) (y : X) := dist_triangle _ _ _      _ <  4 * D ^ (k - 1) + 2 * D ^ k := add_lt_add this hy'      _ ≤ 1 * D ^ (k - 1 + 1) + 2 * D ^ k := by        simp only [one_mul, add_le_add_iff_right]        rw [zpow_add₀ (realD_pos a).ne' _ 1,zpow_one, mul_comm _ (D : ℝ)]        gcongr        exact four_le_realD X      _ ≤ 4 * D ^ k := by        rw [sub_add_cancel, ← right_distrib]        gcongr        norm_num