I3_prop_2

lemma I3_prop_2 {k : ℤ} (hk : -S ≤ k) :      ball o (4 * D ^ S - 2 * D ^ k) ⊆ ⋃ (y : Yk X k), I3 hk y := by    intro x hx    by_cases hx_mem_Xk : x ∈ Xk hk    · rw [Xk] at hx_mem_Xk      simp only [mem_iUnion] at hx_mem_Xk ⊢      refine hx_mem_Xk.elim (fun y hy ↦ ?_)      use y      rw [I3]      exact mem_union_left _ hy    · simp only [mem_iUnion]      have : x ∈ ⋃ (y : Yk X k), I2 hk y := I2_prop_2 hk hx      simp only [mem_iUnion] at this      have : {i | x ∈ I2 hk i}.Nonempty := this      have H := (@wellFounded_lt (Yk X k) _ _)      let y := H.min {i | x ∈ I2 hk i} this      have hy_i2 : x ∈ I2 hk y := H.min_mem {i|x ∈ I2 hk i} this      have hy_is_min : ∀ y', x ∈ I2 hk y' → ¬ y' < y :=        fun y' hy' ↦ H.not_lt_min {i | x ∈ I2 hk i} hy'      use y      revert hy_i2 hy_is_min      generalize y = y      intro hy_i2 hy_min      rw [I3]      have hx_notMem_i1 : ∀ y',x ∉ I1 hk y' := by        simp only [Xk,mem_iUnion, not_exists] at hx_mem_Xk        exact hx_mem_Xk      push _ ∈ _      simp only [not_or, not_exists]      refine Or.inr ⟨hy_i2,hx_mem_Xk, fun y' hy' ↦ ?_⟩      rw [I3]      push _ ∈ _      simp only [not_or, not_exists, not_and]      exact ⟨hx_notMem_i1 y', fun hy_i2' _ _ ↦ hy_min y' hy_i2' hy'⟩