Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ.inr
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      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 (b ^ 2) fuel).fst = n / b ^ (2 * (go n (b ^ 2) fuel).snd)
ih₂ : b ^ (2 * (go n (b ^ 2) fuel).snd) ≤ n
ih₃ : n < b ^ (2 * (go n (b ^ 2) fuel).snd + 2)
⊢ (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
          (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
        else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).fst =
      n /
        b ^
          (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
            else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd ∧
    b ^
          (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
            else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd ≤
        n ∧
      n <
        b ^
          ((if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
                (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
              else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd +
            1)

Tactic:
split

Goal state after:
case succ.inr.isTrue
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      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 (b ^ 2) fuel).fst = n / b ^ (2 * (go n (b ^ 2) fuel).snd)
ih₂ : b ^ (2 * (go n (b ^ 2) fuel).snd) ≤ n
ih₃ : n < b ^ (2 * (go n (b ^ 2) fuel).snd + 2)
h✝ : n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1)
⊢ (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd).fst =
      n / b ^ (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd).snd ∧
    b ^ (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd).snd ≤ n ∧
      n < b ^ ((n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd).snd + 1)

case succ.inr.isFalse
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      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 (b ^ 2) fuel).fst = n / b ^ (2 * (go n (b ^ 2) fuel).snd)
ih₂ : b ^ (2 * (go n (b ^ 2) fuel).snd) ≤ n
ih₃ : n < b ^ (2 * (go n (b ^ 2) fuel).snd + 2)
h✝ : ¬n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1)
⊢ (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1).fst =
      n / b ^ (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1).snd ∧
    b ^ (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1).snd ≤ n ∧
      n < b ^ ((n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1).snd + 1)