case h
b : ℕ
hb : 1 < b
y✝ x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y
b : ℕ
hb : 1 < b
x y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y
induction' x using Nat.strong_induction_on with x ih generalizing y
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ b ^ zero ↔ clog b x ≤ zero

case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
case h
b : ℕ
hb : 1 < b
y✝ x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y
cases y
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
have b_pos : 0 < b := (zero_lt_one' ℕ).trans hb
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔
    (if h : 1 < b ∧ 1 < x then
        let_fun this := (_ : (x + b - 1) / b < x);
        clog b ((x + b - 1) / b) + 1
      else 0) ≤
      succ n✝
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
rw [clog]
case h.succ.inl
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : 1 < b ∧ 1 < x
⊢ x ≤ b ^ succ n✝ ↔
    (let_fun this := (_ : (x + b - 1) / b < x);
      clog b ((x + b - 1) / b) + 1) ≤
      succ n✝

case h.succ.inr
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : ¬(1 < b ∧ 1 < x)
⊢ x ≤ b ^ succ n✝ ↔ 0 ≤ succ n✝
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔
    (if h : 1 < b ∧ 1 < x then
        let_fun this := (_ : (x + b - 1) / b < x);
        clog b ((x + b - 1) / b) + 1
      else 0) ≤
      succ n✝
split_ifs with h
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ 1 ↔ clog b x ≤ zero
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ b ^ zero ↔ clog b x ≤ zero
rw [pow_zero]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ clog b x ≤ zero → x ≤ 1
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ 1 ↔ clog b x ≤ zero
refine' ⟨fun h => (clog_of_right_le_one h b).le, _⟩
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ ¬zero < clog b x → ¬1 < x
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ clog b x ≤ zero → x ≤ 1
simp_rw [← not_lt]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ 1 < x → zero < clog b x
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ ¬zero < clog b x → ¬1 < x
contrapose!
no goals
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ 1 < x → zero < clog b x
exact clog_pos hb
no goals
case h.succ.inl
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : 1 < b ∧ 1 < x
⊢ x ≤ b ^ succ n✝ ↔
    (let_fun this := (_ : (x + b - 1) / b < x);
      clog b ((x + b - 1) / b) + 1) ≤
      succ n✝
rw [succ_eq_add_one, add_le_add_iff_right, ← ih ((x + b - 1) / b) (add_pred_div_lt hb h.2),
  Nat.div_le_iff_le_mul_add_pred b_pos, mul_comm b, ← pow_succ,
  add_tsub_assoc_of_le (Nat.succ_le_of_lt b_pos), add_le_add_iff_right]
no goals
case h.succ.inr
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : ¬(1 < b ∧ 1 < x)
⊢ x ≤ b ^ succ n✝ ↔ 0 ≤ succ n✝
exact iff_of_true ((not_lt.1 (not_and.1 h hb)).trans <| succ_le_of_lt <| pow_pos b_pos _)
  (zero_le _)