Module: Mathlib.Data.Nat.Log

Goal state before:
pp: 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)

pp: 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)

Tactic:
<;>

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)