Real.inv_dyadicRadius_rpow_eq

lemma inv_dyadicRadius_rpow_eq (r0 τ : ℝ) (k : ℕ) (hr0 : 0 ≤ r0) :    (r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ =      (r0⁻¹ : ℝ) ^ τ * ((2 : ℝ) ^ (-τ)) ^ k := by  have h2k_nonneg : 0 ≤ (2 : ℝ) ^ (k : ℝ) :=    le_of_lt (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2) _)  calc    (r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ =        (r0 * (2 : ℝ) ^ (k : ℝ)) ^ (-τ) := by      simpa using (Real.rpow_neg_eq_inv_rpow (r0 * (2 : ℝ) ^ (k : ℝ)) τ).symm    _ = r0 ^ (-τ) * (((2 : ℝ) ^ (k : ℝ)) ^ (-τ)) := by      simpa using (Real.mul_rpow hr0 h2k_nonneg (z := -τ))    _ = (r0⁻¹ : ℝ) ^ τ * ((2 : ℝ) ^ (-τ)) ^ k := by      have hr0' : r0 ^ (-τ) = (r0⁻¹ : ℝ) ^ τ := by        simp [Real.rpow_neg_eq_inv_rpow]      have h2' : ((2 : ℝ) ^ (k : ℝ)) ^ (-τ) = ((2 : ℝ) ^ (-τ)) ^ k := by        have h2nonneg : (0 : ℝ) ≤ (2 : ℝ) := by norm_num        calc          ((2 : ℝ) ^ (k : ℝ)) ^ (-τ) = (2 : ℝ) ^ ((k : ℝ) * (-τ)) := by            exact (Real.rpow_mul (x := (2 : ℝ)) (y := (k : ℝ)) (z := -τ)              h2nonneg).symm          _ = (2 : ℝ) ^ ((-τ) * (k : ℝ)) := by ring_nf          _ = ((2 : ℝ) ^ (-τ)) ^ (k : ℝ) := by            exact Real.rpow_mul (x := (2 : ℝ)) (y := -τ) (z := (k : ℝ)) h2nonneg          _ = ((2 : ℝ) ^ (-τ)) ^ k := by            simp [Real.rpow_natCast]      calc        r0 ^ (-τ) * (((2 : ℝ) ^ (k : ℝ)) ^ (-τ))            = (r0⁻¹ : ℝ) ^ τ * (((2 : ℝ) ^ (k : ℝ)) ^ (-τ)) := by              rw [hr0']        _ = (r0⁻¹ : ℝ) ^ τ * ((2 : ℝ) ^ (-τ)) ^ k := by              rw [h2']