-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem floor_logb_natCast {b : ℕ} {r : ℝ} (hr : 0 ≤ r) :
    ⌊logb b r⌋ = Int.log b r

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

Tactic:
rw [Int.le_floor, le_logb_iff_rpow_le hb1' hr, rpow_intCast]

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

Proof state:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌊logb (↑b) r⌋ = Int.log 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.log b r

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

Proof state:
b : ℕ
r : ℝ
hr : 0 ≤ r
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
obtain rfl | hr := hr.eq_or_lt

Result:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌊logb (↑b) 0⌋ = Int.log b 0

case inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
⊢ ⌊logb (↑b) r⌋ = Int.log b r

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

Tactic:
simp_all only [Nat.cast_one, logb_one_left, Int.floor_zero, Int.log_one_left]

Result:
no goals

Proof state:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌊logb (↑b) 0⌋ = Int.log b 0

Tactic:
rw [logb_zero, Int.log_zero_right, Int.floor_zero]

Result:
no goals

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

Tactic:
exact Int.zpow_log_le_self hb hr

Result:
no goals

Proof state:
case inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
⊢ ⌊logb (↑b) r⌋ = Int.log 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.log b r

case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Proof state:
case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌊logb (↑b) r⌋ = Int.log 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.log 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.log b r

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

Result:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ ↑⌊logb (↑b) r⌋ ≤ 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.floor_le _)

Result:
no goals

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

Tactic:
cases hb

Result:
case neg.inl
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 0
⊢ ⌊logb (↑b) r⌋ = Int.log b r

case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Proof state:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌊logb (↑b) r⌋ = Int.log 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.log b r

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

Tactic:
simp_all only [CharP.cast_eq_zero, logb_zero_left, Int.floor_zero, Int.log_zero_left]

Result:
no goals

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

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

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