-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
rw :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) /
        HPow.hPow (α := ℝ) 2 (n + 1)|
rw₁ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
          HPow.hPow (α := ℝ) 2 (n + 1) -
        HDiv.hDiv (α := ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
          (HPow.hPow (α := ℝ) 2 (n + 1))|
rw₂ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ (HPow.hPow (α := ℕ) 2 n * 2) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
          HPow.hPow (α := ℝ) 2 (n + 1) -
        HDiv.hDiv (α := ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
          (HPow.hPow (α := ℝ) 2 (n + 1))|
rw₃ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ (HPow.hPow (α := ℕ) 2 n * 2) : (a : ℝ) → ℝ) 0 : ℝ) (2 * HPow.hPow (α := ℝ) 2 n)| =
    |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
          (2 * HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
          (2 * HPow.hPow (α := ℝ) 2 n)|
rw₄ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ (HPow.hPow (α := ℕ) 2 n * 2) : (a : ℝ) → ℝ) 0 : ℝ) (2 * HPow.hPow (α := ℝ) 2 n)| =
    |HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
          (2 * HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
          (2 * HPow.hPow (α := ℝ) 2 n)|
⊢ |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)| /
      |HPow.hPow (α := ℝ) 2 (n + 1)|
have rw₅ : |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
      HDiv.hDiv (α := ℝ) ((f ^ (HPow.hPow (α := ℕ) 2 n * 2) : (a : ℝ) → ℝ) 0 : ℝ) (2 * HPow.hPow (α := ℝ) 2 n)| =
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
      HDiv.hDiv (α := ℝ)
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
        (2 * HPow.hPow (α := ℝ) 2 n)|
Tactic: rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]