awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : logb b 1 < logb b x ↔ x < 1
⊢ 0 < logb b x ↔ x < 1
have rw₁ : x < 1 ↔ x < 1
Tactic: rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one zero_lt_one hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
⊢ logb b x < 0 ↔ 1 < x
have rw : logb b x < logb b 1 ↔ 1 < x
Tactic: rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one h zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
rw : logb b x < logb b 1 ↔ 1 < x
⊢ logb b x < 0 ↔ 1 < x
have rw₁ : 1 < x ↔ 1 < x
Tactic: rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one h zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 ≤ logb b x ↔ x ≤ 1
have rw : ¬logb b x < 0 ↔ x ≤ 1
Tactic: rw [← not_lt, logb_neg_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : ¬logb b x < 0 ↔ x ≤ 1
⊢ 0 ≤ logb b x ↔ x ≤ 1
have rw₁ : ¬1 < x ↔ x ≤ 1
Tactic: rw [← not_lt, logb_neg_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : ¬logb b x < 0 ↔ x ≤ 1
rw₁ : ¬1 < x ↔ x ≤ 1
⊢ 0 ≤ logb b x ↔ x ≤ 1
have rw₂ : x ≤ 1 ↔ x ≤ 1
Tactic: rw [← not_lt, logb_neg_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ 0 ↔ 1 ≤ x
have rw : ¬0 < logb b x ↔ 1 ≤ x
Tactic: rw [← not_lt, logb_pos_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : ¬0 < logb b x ↔ 1 ≤ x
⊢ logb b x ≤ 0 ↔ 1 ≤ x
have rw₁ : ¬x < 1 ↔ 1 ≤ x
Tactic: rw [← not_lt, logb_pos_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : ¬0 < logb b x ↔ 1 ≤ x
rw₁ : ¬x < 1 ↔ 1 ≤ x
⊢ logb b x ≤ 0 ↔ 1 ≤ x
have rw₂ : 1 ≤ x ↔ 1 ≤ x
Tactic: rw [← not_lt, logb_pos_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y
have rw : logb b |x| < logb b |y|
Tactic: rw [← logb_abs b y, ← logb_abs b x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |x| < logb b |y|
have refine : |y| < |x|
Tactic: refine logb_lt_logb_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|
have rwa : -y < |x|
Tactic: rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
rwa : -y < |x|
⊢ |y| < |x|
have rwa₁ : -y < -x
Tactic: rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ Tendsto (logb b) atTop atBot
have rw : ∀ (b_1 : ℝ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → logb b a ≤ b_1
Tactic: rw [tendsto_atTop_atBot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → logb b a ≤ e
have h : ∀ (a : ℝ), max 1 (b ^ e) ≤ a → logb b a ≤ e
Tactic: use 1 ⊔ b ^ e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ max 1 (b ^ e) ≤ a → logb b a ≤ e
have h : 1 ≤ a → b ^ e ≤ a → logb b a ≤ e
Tactic: simp only [and_imp, sup_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → logb b a ≤ e
have h : b ^ e ≤ a → b ^ e ≤ a
Tactic: rw [logb_le_iff_le_rpow_of_base_lt_one b_pos b_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
h : b ^ e ≤ a → b ^ e ≤ a
⊢ b ^ e ≤ a → logb b a ≤ e
have h₁ : 0 < a
Tactic: rw [logb_le_iff_le_rpow_of_base_lt_one b_pos b_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr : 0 ≤ r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have inl : ∀ (hr : LE.le (α := ℝ) 0 0), ⌊logb (↑b : ℝ) 0⌋ = Int.log (R := ℝ) b 0
Tactic: obtain rfl | hr := hr.eq_or_lt
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr : 0 ≤ r
inl : ∀ (hr : LE.le (α := ℝ) 0 0), ⌊logb (↑b : ℝ) 0⌋ = Int.log (R := ℝ) b 0
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have inr : ∀ (hr : 0 < r), ⌊logb (↑b : ℝ) r⌋ = Int.log b r
Tactic: obtain rfl | hr := hr.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
hr : LE.le (α := ℝ) 0 0
⊢ ⌊logb (↑b : ℝ) 0⌋ = Int.log (R := ℝ) b 0
have inl : Int.floor (α := ℝ) 0 = Int.log (R := ℝ) b 0
Tactic: rw [logb_zero, Int.log_zero_right, Int.floor_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
hr : LE.le (α := ℝ) 0 0
inl : Int.floor (α := ℝ) 0 = Int.log (R := ℝ) b 0
⊢ ⌊logb (↑b : ℝ) 0⌋ = Int.log (R := ℝ) b 0
have inl₁ : Int.floor (α := ℝ) 0 = 0
Tactic: rw [logb_zero, Int.log_zero_right, Int.floor_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
hr : LE.le (α := ℝ) 0 0
inl : Int.floor (α := ℝ) 0 = Int.log (R := ℝ) b 0
inl₁ : Int.floor (α := ℝ) 0 = 0
⊢ ⌊logb (↑b : ℝ) 0⌋ = Int.log (R := ℝ) b 0
have inl₂ : Eq (α := ℤ) 0 0
Tactic: rw [logb_zero, Int.log_zero_right, Int.floor_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have pos : ∀ (hb : 1 < b), ⌊logb (↑b : ℝ) r⌋ = Int.log b r
Tactic: by_cases hb : 1 < b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
pos : ∀ (hb : 1 < b), ⌊logb (↑b : ℝ) r⌋ = Int.log b r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have neg : ∀ (hb : ¬1 < b), ⌊logb (↑b : ℝ) r⌋ = Int.log b r
Tactic: by_cases hb : 1 < b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (hypothesis)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
Tactic: have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have pos : ⌊logb (↑b : ℝ) r⌋ ≤ Int.log b r
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
pos : ⌊logb (↑b : ℝ) r⌋ ≤ Int.log b r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have pos₁ : Int.log b r ≤ ⌊logb (↑b : ℝ) r⌋
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ ⌊logb (↑b : ℝ) r⌋ ≤ Int.log b r
have pos : HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌊logb (↑b : ℝ) r⌋ : ℝ) ≤ r
Tactic: rw [← Int.zpow_le_iff_le_log hb hr, ← rpow_intCast b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌊logb (↑b : ℝ) r⌋ : ℝ) ≤ r
have pos : HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌊logb (↑b : ℝ) r⌋ : ℝ) ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (logb (↑b : ℝ) r)
Tactic: refine le_of_le_of_eq ?_ (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Int.log b r ≤ ⌊logb (↑b : ℝ) r⌋
have pos : HPow.hPow (α := ℝ) (↑b : ℝ) (Int.log b r) ≤ r
Tactic: rw [Int.le_floor, le_logb_iff_rpow_le hb1' hr, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (hypothesis)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have hb₁ : b = 0 ∨ b = 1
Tactic: rw [Nat.one_lt_iff_ne_zero_and_ne_one, ← or_iff_not_and_not] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have neg : b = 0 → ⌊logb (↑b : ℝ) r⌋ = Int.log b r
Tactic: cases hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
neg : b = 0 → ⌊logb (↑b : ℝ) r⌋ = Int.log b r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r
have neg₁ : b = 1 → ⌊logb (↑b : ℝ) r⌋ = Int.log b r
Tactic: cases hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr : 0 ≤ r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have inl : ∀ (hr : LE.le (α := ℝ) 0 0), ⌈logb (↑b : ℝ) 0⌉ = Int.clog (R := ℝ) b 0
Tactic: obtain rfl | hr := hr.eq_or_lt
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr : 0 ≤ r
inl : ∀ (hr : LE.le (α := ℝ) 0 0), ⌈logb (↑b : ℝ) 0⌉ = Int.clog (R := ℝ) b 0
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have inr : ∀ (hr : 0 < r), ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
Tactic: obtain rfl | hr := hr.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
hr : LE.le (α := ℝ) 0 0
⊢ ⌈logb (↑b : ℝ) 0⌉ = Int.clog (R := ℝ) b 0
have inl : Int.ceil (α := ℝ) 0 = Int.clog (R := ℝ) b 0
Tactic: rw [logb_zero, Int.clog_zero_right, Int.ceil_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
hr : LE.le (α := ℝ) 0 0
inl : Int.ceil (α := ℝ) 0 = Int.clog (R := ℝ) b 0
⊢ ⌈logb (↑b : ℝ) 0⌉ = Int.clog (R := ℝ) b 0
have inl₁ : Int.ceil (α := ℝ) 0 = 0
Tactic: rw [logb_zero, Int.clog_zero_right, Int.ceil_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
hr : LE.le (α := ℝ) 0 0
inl : Int.ceil (α := ℝ) 0 = Int.clog (R := ℝ) b 0
inl₁ : Int.ceil (α := ℝ) 0 = 0
⊢ ⌈logb (↑b : ℝ) 0⌉ = Int.clog (R := ℝ) b 0
have inl₂ : Eq (α := ℤ) 0 0
Tactic: rw [logb_zero, Int.clog_zero_right, Int.ceil_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have pos : ∀ (hb : 1 < b), ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
Tactic: by_cases hb : 1 < b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
pos : ∀ (hb : 1 < b), ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have neg : ∀ (hb : ¬1 < b), ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
Tactic: by_cases hb : 1 < b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (hypothesis)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
Tactic: have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have pos : ⌈logb (↑b : ℝ) r⌉ ≤ Int.clog b r
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
pos : ⌈logb (↑b : ℝ) r⌉ ≤ Int.clog b r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have pos₁ : Int.clog b r ≤ ⌈logb (↑b : ℝ) r⌉
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ ⌈logb (↑b : ℝ) r⌉ ≤ Int.clog b r
have pos : r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (Int.clog b r)
Tactic: rw [Int.ceil_le, logb_le_iff_le_rpow hb1' hr, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Int.clog b r ≤ ⌈logb (↑b : ℝ) r⌉
have pos : r ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)
Tactic: rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_intCast b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ r ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)
have pos : HPow.hPow (α := ℝ) (↑b : ℝ) (logb (↑b : ℝ) r) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)
Tactic: refine (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (hypothesis)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have hb₁ : b = 0 ∨ b = 1
Tactic: rw [Nat.one_lt_iff_ne_zero_and_ne_one, ← or_iff_not_and_not] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have neg : b = 0 → ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
Tactic: cases hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
neg : b = 0 → ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
have neg₁ : b = 1 → ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
Tactic: cases hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b n : ℕ
⊢ ⌊logb (↑b : ℝ) (↑n : ℝ)⌋₊ = Nat.log b n
have zero : ⌊logb (↑0 : ℝ) (↑n : ℝ)⌋₊ = Nat.log 0 n
Tactic: obtain _ | _ | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b n : ℕ
zero : ⌊logb (↑0 : ℝ) (↑n : ℝ)⌋₊ = Nat.log 0 n
⊢ ⌊logb (↑b : ℝ) (↑n : ℝ)⌋₊ = Nat.log b n
have succ : ⌊logb (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (HAdd.hAdd (α := ℕ) 0 1) n
Tactic: obtain _ | _ | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b n : ℕ
zero : ⌊logb (↑0 : ℝ) (↑n : ℝ)⌋₊ = Nat.log 0 n
succ : ⌊logb (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (HAdd.hAdd (α := ℕ) 0 1) n
⊢ ⌊logb (↑b : ℝ) (↑n : ℝ)⌋₊ = Nat.log b n
have succ₁ : ∀ (b : ℕ), ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n
Tactic: obtain _ | _ | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
n b : ℕ
⊢ ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n
have succ : ⌊logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌋₊ = Nat.log (b + 1 + 1) 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
n b : ℕ
succ : ⌊logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌋₊ = Nat.log (b + 1 + 1) 0
⊢ ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n
have succ₁ : ∀ (hn : n ≠ 0), ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
n b : ℕ
hn : n ≠ 0
⊢ ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n
have succ : 0 ≤ logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℤ), Int.natCast_floor_eq_floor, floor_logb_natCast (by simp),
    Int.log_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b n : ℕ
⊢ ⌈logb (↑b : ℝ) (↑n : ℝ)⌉₊ = Nat.clog b n
have zero : ⌈logb (↑0 : ℝ) (↑n : ℝ)⌉₊ = Nat.clog 0 n
Tactic: obtain _ | _ | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b n : ℕ
zero : ⌈logb (↑0 : ℝ) (↑n : ℝ)⌉₊ = Nat.clog 0 n
⊢ ⌈logb (↑b : ℝ) (↑n : ℝ)⌉₊ = Nat.clog b n
have succ : ⌈logb (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (HAdd.hAdd (α := ℕ) 0 1) n
Tactic: obtain _ | _ | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b n : ℕ
zero : ⌈logb (↑0 : ℝ) (↑n : ℝ)⌉₊ = Nat.clog 0 n
succ : ⌈logb (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (HAdd.hAdd (α := ℕ) 0 1) n
⊢ ⌈logb (↑b : ℝ) (↑n : ℝ)⌉₊ = Nat.clog b n
have succ₁ : ∀ (b : ℕ), ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n
Tactic: obtain _ | _ | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
n b : ℕ
⊢ ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n
have succ : ⌈logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌉₊ = Nat.clog (b + 1 + 1) 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
n b : ℕ
succ : ⌈logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌉₊ = Nat.clog (b + 1 + 1) 0
⊢ ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n
have succ₁ : ∀ (hn : n ≠ 0), ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
n b : ℕ
hn : n ≠ 0
⊢ ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n
have succ : 0 ≤ logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℤ), Int.natCast_ceil_eq_ceil, ceil_logb_natCast (by simp),
    Int.clog_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℕ
⊢ (↑(Nat.log b a) : ℝ) ≤ logb (↑b : ℝ) (↑a : ℝ)
have apply : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑⌊logb (↑b : ℝ) (↑a : ℝ)⌋ : ℝ)
Tactic: apply le_trans _ (Int.floor_le ((b : ℝ).logb a))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℕ
⊢ LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑⌊logb (↑b : ℝ) (↑a : ℝ)⌋ : ℝ)
have rw : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑(Int.log (R := ℝ) b (↑a : ℝ)) : ℝ)
Tactic: rw [Real.floor_logb_natCast (Nat.cast_nonneg a), Int.log_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℕ
rw : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑(Int.log (R := ℝ) b (↑a : ℝ)) : ℝ)
⊢ LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑⌊logb (↑b : ℝ) (↑a : ℝ)⌋ : ℝ)
have rw₁ : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑(↑(Nat.log b a) : ℤ) : ℝ)
Tactic: rw [Real.floor_logb_natCast (Nat.cast_nonneg a), Int.log_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℕ
rw : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑(Int.log (R := ℝ) b (↑a : ℝ)) : ℝ)
rw₁ : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑(↑(Nat.log b a) : ℤ) : ℝ)
⊢ LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑⌊logb (↑b : ℝ) (↑a : ℝ)⌋ : ℝ)
have rw₂ : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑(Nat.log b a) : ℝ)
Tactic: rw [Real.floor_logb_natCast (Nat.cast_nonneg a), Int.log_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have simp_rw : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: simp_rw [logb, div_eq_zero_iff, log_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto