-- Mathlib/Data/Nat/Log.lean
theorem le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x y : ℕ} : x ≤ b ^ y ↔ clog b x ≤ y

Proof state:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ clog b x ≤ 0 → x ≤ 1

Tactic:
simp_rw [← not_lt]

Result:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ ¬0 < clog b x → ¬1 < x

Proof state:
case pos
b : ℕ
hb : 1 < b
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 ^ (n✝ + 1) ↔ clog b ((x + b - 1) / b) + 1 ≤ n✝ + 1

Tactic:
rw [Nat.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, Nat.mul_comm b, ← Nat.pow_succ,
  Nat.add_sub_assoc (Nat.succ_le_of_lt b_pos), Nat.add_le_add_iff_right]

Result:
no goals

Proof state:
case h.succ
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
⊢ x ≤ b ^ (n✝ + 1) ↔ clog b x ≤ n✝ + 1

Tactic:
have b_pos : 0 < b := zero_lt_of_lt hb

Result:
case h.succ
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ (n✝ + 1) ↔ clog b x ≤ n✝ + 1

Proof state:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ b ^ 0 ↔ clog b x ≤ 0

Tactic:
rw [Nat.pow_zero]

Result:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ 1 ↔ clog b x ≤ 0

Proof state:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ 1 ↔ clog b x ≤ 0

Tactic:
refine ⟨fun h => (clog_of_right_le_one h b).le, ?_⟩

Result:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ clog b x ≤ 0 → x ≤ 1

Proof state:
b : ℕ
hb : 1 < b
x y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y

Tactic:
induction x using Nat.strong_induction_on generalizing y with | h x ih => ?_

Result:
case h
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y

Proof state:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ 1 < x → 0 < clog b x

Tactic:
exact clog_pos hb

Result:
no goals

Proof state:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ ¬0 < clog b x → ¬1 < x

Tactic:
contrapose!

Result:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ 1 < x → 0 < clog b x

Proof state:
case h
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y

Tactic:
cases y

Result:
case h.zero
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ b ^ 0 ↔ clog b x ≤ 0

case h.succ
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
⊢ x ≤ b ^ (n✝ + 1) ↔ clog b x ≤ n✝ + 1

Proof state:
case h.succ
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ (n✝ + 1) ↔ clog b x ≤ n✝ + 1

Tactic:
rw [clog]

Result:
case h.succ
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ (n✝ + 1) ↔ (if h : 1 < b ∧ 1 < x then clog b ((x + b - 1) / b) + 1 else 0) ≤ n✝ + 1

Proof state:
case h.succ
b : ℕ
hb : 1 < b
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ (n✝ + 1) ↔ (if h : 1 < b ∧ 1 < x then clog b ((x + b - 1) / b) + 1 else 0) ≤ n✝ + 1

Tactic:
split_ifs with h

Result:
case pos
b : ℕ
hb : 1 < b
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 ^ (n✝ + 1) ↔ clog b ((x + b - 1) / b) + 1 ≤ n✝ + 1

case neg
b : ℕ
hb : 1 < b
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 ^ (n✝ + 1) ↔ 0 ≤ n✝ + 1

Proof state:
case neg
b : ℕ
hb : 1 < b
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 ^ (n✝ + 1) ↔ 0 ≤ n✝ + 1

Tactic:
exact iff_of_true ((not_lt.1 (not_and.1 h hb)).trans <| succ_le_of_lt <| Nat.pow_pos b_pos)
  (zero_le _)

Result:
no goals