calculation_12

lemma calculation_12 (s : ℝ) :    128 * (D : ℝ)^(s + 2) = 2^(2 * 𝕔 * a ^ 2 + 4) * (8 * D ^ s) := by  simp only [defaultD]  have leftSide := calc 128 * ((2 : ℝ) ^ (𝕔 * a ^ 2)) ^ (s + 2)    _ = 128 * 2^(𝕔 * a^2 * (s + 2)) := by      congrm 128 * ?_      have fact := Real.rpow_mul (x := 2) (y := 𝕔 * a ^ 2) (z := s + 2) (by positivity)      rw_mod_cast [fact]    _ = 128 * 2^((𝕔 * a^2 * s) + (𝕔 * a^2 * 2)) := by      congrm 128 * (2 ^ ?_)      ring    _ = (2 ^ 7) * 2^((𝕔 * a^2 * s) + (𝕔 * a^2 * 2)) := by      norm_num    _ = 2 ^ (7 + ((𝕔 * a^2 * s) + (𝕔 * a^2 * 2))) := by      have fact := Real.rpow_add (x := 2) (y := 7) (z := 𝕔 * a^2 * s + 𝕔 * a^2 * 2) (by positivity)      rw_mod_cast [fact]  have rightSide := calc 2 ^ (2 * 𝕔 * a ^ 2 + 4) * (8 * ((2 : ℝ) ^ (𝕔 * a ^ 2)) ^ s)    _ = 2 ^ (2 * 𝕔 *a^2 + 4) * ((2^3)*((2 ^ (𝕔 * a ^ 2)) ^ s)) := by      norm_num    _ = 2 ^ (2 * 𝕔 *a^2 + 4) * (  2^3 * 2 ^ (𝕔 * a ^ 2 * s)  ) := by      rw [Real.rpow_mul (x:=2) (by positivity)]      norm_cast    _ = 2 ^ (2 * 𝕔 * a^2 + 4) * 2 ^ (3 + 𝕔 * a ^ 2 * s) := by      have fact := Real.rpow_add (x:=2) (y:= 3) (z:= 𝕔 * a ^ 2 * s) (by positivity)      rw_mod_cast [fact]    _ = 2 ^ (2 * 𝕔 * a^2 + 4  + (3 + 𝕔 * a ^ 2 * s)) := by      nth_rw 2 [Real.rpow_add]      · norm_cast      · positivity    _ = 2 ^ (7 + ((𝕔 * a^2 * s) + (𝕔 * a^2 * 2))) := by      congrm 2 ^ ?_      linarith  rw_mod_cast [leftSide]  rw_mod_cast [rightSide]