case h
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
x : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
induction' y using Nat.strong_induction_on with y ih generalizing x
no goals
case h.zero
b : ℕ
hb : 1 < b
x y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ b ^ zero ≤ y ↔ zero ≤ log b y
exact iff_of_true hy.bot_lt (zero_le _)
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      if h : b ≤ y ∧ 1 < b then
        let_fun this := (_ : y / b < y);
        log b (y / b) + 1
      else 0
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔ succ x ≤ log b y
rw [log]
case h.succ.inl
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1

case h.succ.inr
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : ¬(b ≤ y ∧ 1 < b)
⊢ b ^ succ x ≤ y ↔ succ x ≤ 0
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      if h : b ≤ y ∧ 1 < b then
        let_fun this := (_ : y / b < y);
        log b (y / b) + 1
      else 0
split_ifs with h
case h.succ.inl
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
b_pos : 0 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1
case h.succ.inl
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1
have b_pos : 0 < b := zero_le_one.trans_lt hb
no goals
case h.succ.inl
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
b_pos : 0 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1
rw [succ_eq_add_one, add_le_add_iff_right, ←
  ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne', le_div_iff_mul_le b_pos,
  pow_succ', mul_comm]
no goals
case h.succ.inr
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : ¬(b ≤ y ∧ 1 < b)
⊢ b ^ succ x ≤ y ↔ succ x ≤ 0
exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩)
  (not_succ_le_zero _)