S_spec

lemma S_spec : ∃ n : ℕ, (∀ x, -n ≤ σ₁ x ∧ σ₂ x ≤ n) ∧    F ⊆ ball (cancelPt X) (defaultD a ^ n / 4) ∧    G ⊆ ball (cancelPt X) (defaultD a ^ n / 4) ∧ 0 < n := by  obtain ⟨l₁, hl₁⟩ := bddBelow_def.mp (Finite.bddBelow (finite_range_σ₁ (X := X)))  obtain ⟨u₂, hu₂⟩ := bddAbove_def.mp (Finite.bddAbove (finite_range_σ₂ (X := X)))  simp_rw [mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hl₁ hu₂  have one_lt_D := one_lt_realD X  obtain ⟨rF, rFpos, hrF⟩ : ∃ r > 0, F ⊆ ball (cancelPt X) r := by    obtain ⟨r, hr⟩ := isBounded_F.subset_ball (cancelPt X)    rcases lt_or_ge 0 r with lr | lr    · use r    · use 1, zero_lt_one, hr.trans (ball_subset_ball (lr.trans zero_le_one))  let nF := ⌈Real.logb (defaultD a) (4 * rF)⌉  obtain ⟨rG, rGpos, hrG⟩ : ∃ r > 1, G ⊆ ball (cancelPt X) r := by    obtain ⟨r, hr⟩ := isBounded_G.subset_ball (cancelPt X)    rcases lt_or_ge 0 r with lr | lr    · use r + 1, by linarith, subset_trans hr (ball_subset_ball (by simp))    · use 2, one_lt_two, hr.trans (ball_subset_ball (lr.trans zero_le_two))  let nG := ⌈Real.logb (defaultD a) (4 * rG)⌉  refine ⟨(max (max (-l₁) u₂) (max nF nG)).toNat, ⟨fun x ↦ ?_, ?_, ?_, ?_⟩⟩  · simp only [Int.ofNat_toNat, ← min_neg_neg, neg_neg, min_le_iff, le_max_iff]    exact ⟨.inl (.inl (.inl (hl₁ x))), .inl (.inl (.inr (hu₂ x)))⟩  · refine hrF.trans (ball_subset_ball ?_)    trans (defaultD a : ℝ) ^ nF / 4    · rw [le_div_iff₀' zero_lt_four, ← Real.rpow_intCast,          ← Real.logb_le_iff_le_rpow one_lt_D (by positivity)]      exact Int.le_ceil _    rw [← Real.rpow_natCast, ← Real.rpow_intCast]    gcongr    · exact one_lt_D.le    norm_cast    apply Int.self_le_toNat nF |>.trans    exact_mod_cast Int.toNat_le_toNat <| (le_max_left ..).trans <| le_max_right ..  · refine hrG.trans (ball_subset_ball ?_)    trans (defaultD a : ℝ) ^ nG / 4    · rw [le_div_iff₀' zero_lt_four, ← Real.rpow_intCast,          ← Real.logb_le_iff_le_rpow one_lt_D (by positivity)]      exact Int.le_ceil _    rw [← Real.rpow_natCast, ← Real.rpow_intCast]    gcongr    · exact one_lt_D.le    norm_cast    apply Int.self_le_toNat nG |>.trans    exact_mod_cast Int.toNat_le_toNat <| (le_max_right ..).trans <| le_max_right ..  · apply Int.pos_iff_toNat_pos.mp <| lt_of_lt_of_le _ <| (le_max_right ..).trans <| le_max_right ..    exact Int.ceil_pos.mpr (Real.logb_pos one_lt_D (by linarith))