-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem ceil_logb_natCast {b : ℕ} {r : ℝ} (hr : 0 ≤ r) :
    ⌈logb b r⌉ = Int.clog b r

Proof state:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ logb (↑b) r ≤ ↑b ^ ↑⌈logb (↑b) r⌉

Tactic:
exact rpow_le_rpow_of_exponent_le hb1'.le (Int.le_ceil _)

Result:
no goals

Proof state:
case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
cases hb

Result:
case neg.inl
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 0
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Proof state:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉

Tactic:
rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_intCast b]

Result:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ ↑⌈logb (↑b) r⌉

Proof state:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ ≤ Int.clog b r

Tactic:
rw [Int.ceil_le, logb_le_iff_le_rpow hb1' hr, rpow_intCast]

Result:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ Int.clog b r

Proof state:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ ↑⌈logb (↑b) r⌉

Tactic:
refine (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le ?_

Result:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ logb (↑b) r ≤ ↑b ^ ↑⌈logb (↑b) r⌉

Proof state:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
apply le_antisymm

Result:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ ≤ Int.clog b r

case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉

Proof state:
case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
simp_all only [Nat.cast_one, logb_one_left, Int.ceil_zero, Int.clog_one_left]

Result:
no goals

Proof state:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌈logb (↑b) 0⌉ = Int.clog b 0

Tactic:
rw [logb_zero, Int.clog_zero_right, Int.ceil_zero]

Result:
no goals

Proof state:
case inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
by_cases hb : 1 < b

Result:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Proof state:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb

Result:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Proof state:
case neg.inl
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 0
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
simp_all only [CharP.cast_eq_zero, logb_zero_left, Int.ceil_zero, Int.clog_zero_left]

Result:
no goals

Proof state:
case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
rw [Nat.one_lt_iff_ne_zero_and_ne_one, ← or_iff_not_and_not] at hb

Result:
case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Proof state:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ Int.clog b r

Tactic:
exact Int.self_le_zpow_clog hb r

Result:
no goals

Proof state:
b : ℕ
r : ℝ
hr : 0 ≤ r
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
obtain rfl | hr := hr.eq_or_lt

Result:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌈logb (↑b) 0⌉ = Int.clog b 0

case inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
⊢ ⌈logb (↑b) r⌉ = Int.clog b r