calculation_4

lemma calculation_4 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]    {s_1 s_2 s_3 : ℤ} {dist_a dist_b dist_c dist_d : ℝ}    (lt_1 : dist_a < 100 * D ^ (s_1 + 3))    (lt_2 : dist_b < 8 * D ^ s_3)    (lt_3 : dist_c < 8⁻¹ * D ^ s_1)    (lt_4 : dist_d < 4 * D ^ s_2)    (three : s_1 + 3 < s_3) (plusOne : s_2 = s_1 + 1) :    dist_a + dist_d + dist_c + dist_b < 10 * D ^ s_3 := by  calc dist_a + dist_d + dist_c + dist_b  _ ≤ 100 * D ^ (s_1 + 3) + dist_d + dist_c + dist_b := by    change dist_a < 100 * D ^ (s_1 + 3) at lt_1    gcongr  _ ≤ 100 * D ^ (s_1 + 3) + 4 * D ^ (s_1 + 1) + dist_c + dist_b := by    gcongr    apply le_of_lt    rw [← plusOne]    exact lt_4  _ ≤ 100 * D ^ (s_1 + 3) + 4 * D ^ (s_1 + 1) + 8⁻¹ * D ^ s_1 + dist_b := by    gcongr  _ ≤ 100 * D ^ (s_1 + 3) + 4 * D ^ (s_1 + 1) + 8⁻¹ * D ^ s_1 + 8 * D ^ s_3 := by    gcongr  _ = 100 * D ^ (s_1 + 3) + ((4 * D ^ (- 2 : ℝ)) * D ^ (s_1 + 3)) + 8⁻¹ * D ^ s_1 + 8 * D ^ s_3 := by    rw [calculation_1 (s := s_1)]  _ = 100 * D ^ (s_1 + 3) + ((4 * D ^ (- 2 : ℝ)) * D ^ (s_1 + 3)) + (((8 : ℝ)⁻¹ * D ^ (- 3 : ℝ)) * D ^ (s_1 + 3)) + 8 * D ^ s_3 := by    rw [calculation_2 (s := s_1)]  _ < 10 * D ^ s_3 := by    exact calculation_3 (h := three) (X := X)