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