-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) ≤ n
ih₃ : n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 2)
succ :
  n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) →
    (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).fst =
        n /
          b ^
            (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd ∧
      b ^ (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd ≤
          n ∧
        n <
          b ^
            ((n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd),
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd +
              1)
⊢ (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
        else
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
            2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).fst =
      n /
        b ^
          (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
            else
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd ∧
    b ^
          (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
            else
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd ≤
        n ∧
      n <
        b ^
          ((if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
                (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
              else
                (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd +
            1)
have succ₁ : ¬n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) →
  (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).fst =
      n /
        b ^
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
              2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd ∧
    b ^
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
              2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd ≤
        n ∧
      n <
        b ^
          ((n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd +
            1)
Tactic: split