Module: Mathlib.Data.Nat.Log

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

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

Tactic:
<;>

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

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