awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
pos : HPow.hPow (α := ℝ) (↑b : ℝ) (Int.log b r) ≤ r
⊢ Int.log b r ≤ ⌊logb (↑b : ℝ) r⌋

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

Premises used: Real.le_logb_iff_rpow_le, Int.le_floor, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) (Int.log b r) ≤ r

Tactic:
Int.zpow_log_le_self hb hr

Premises used: Int.zpow_log_le_self
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) (Int.log b r) ≤ r

Tactic:
exact Int.zpow_log_le_self hb hr

Premises used: Int.zpow_log_le_self
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ b = 0 ∨ b = 1

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

Premises used: or_iff_not_and_not, Nat.one_lt_iff_ne_zero_and_ne_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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
neg₁ : b = 1 → ⌊logb (↑b : ℝ) r⌋ = Int.log b r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log b r

Tactic:
cases hb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 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]

Premises used: CharP.cast_eq_zero, Real.logb_zero_left, Int.floor_zero, Int.log_zero_left
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 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]

Premises used: Int.log_one_left, Int.floor_zero, Real.logb_one_left, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr : 0 ≤ r
inl : ∀ (hr : LE.le (α := ℝ) 0 0), ⌈logb (↑b : ℝ) 0⌉ = Int.clog (R := ℝ) b 0
inr : ∀ (hr : 0 < r), ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r

Tactic:
obtain rfl | hr := hr.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
hr : LE.le (α := ℝ) 0 0
inl : Int.ceil (α := ℝ) 0 = Int.clog (R := ℝ) b 0
inl₁ : Int.ceil (α := ℝ) 0 = 0
inl₂ inl₃ : Eq (α := ℤ) 0 0
⊢ ⌈logb (↑b : ℝ) 0⌉ = Int.clog (R := ℝ) b 0

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

Premises used: Int.ceil_zero, Real.logb_zero, Int.clog_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
pos : ∀ (hb : 1 < b), ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
neg : ∀ (hb : ¬1 < b), ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r

Tactic:
by_cases hb : 1 < b
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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
pos₁ : Int.clog b r ≤ ⌈logb (↑b : ℝ) r⌉
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
pos : r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (Int.clog b r)
⊢ ⌈logb (↑b : ℝ) r⌉ ≤ Int.clog b r

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

Premises used: Real.logb_le_iff_le_rpow, Int.ceil_le, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (Int.clog b r)

Tactic:
Int.self_le_zpow_clog hb r

Premises used: Int.self_le_zpow_clog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (Int.clog b r)

Tactic:
exact Int.self_le_zpow_clog hb r

Premises used: Int.self_le_zpow_clog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
pos : r ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)
⊢ Int.clog b r ≤ ⌈logb (↑b : ℝ) r⌉

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

Premises used: Nat.cast, Int.le_zpow_iff_clog_le, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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⌉ : ℝ)

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

Premises used: Eq.trans_le, Real.rpow_logb, LT.lt.ne', zero_lt_one, LT.lt.trans, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
pos : HPow.hPow (α := ℝ) (↑b : ℝ) (logb (↑b : ℝ) r) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)
⊢ r ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)

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

Premises used: Eq.trans_le, Real.rpow_logb, LT.lt.ne', zero_lt_one, LT.lt.trans, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) (logb (↑b : ℝ) r) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)

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

Premises used: Int.le_ceil, LT.lt.le, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) (logb (↑b : ℝ) r) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈logb (↑b : ℝ) r⌉ : ℝ)

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

Premises used: Int.le_ceil, LT.lt.le, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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
neg₁ : b = 1 → ⌈logb (↑b : ℝ) r⌉ = Int.clog b r
⊢ ⌈logb (↑b : ℝ) r⌉ = Int.clog b r

Tactic:
cases hb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 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]

Premises used: CharP.cast_eq_zero, Real.logb_zero_left, Int.clog_zero_left, Int.ceil_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 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]

Premises used: Int.clog_one_left, Real.logb_one_left, Int.ceil_zero, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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
succ₁ : ∀ (b : ℕ), ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n
⊢ ⌊logb (↑b : ℝ) (↑n : ℝ)⌋₊ = Nat.log b n

Tactic:
obtain _ | _ | b := b
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n : ℕ
⊢ ⌊logb (↑0 : ℝ) (↑n : ℝ)⌋₊ = Nat.log 0 n

Tactic:
simp [Real.logb]

Premises used: Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n : ℕ
⊢ ⌊logb (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (HAdd.hAdd (α := ℕ) 0 1) n

Tactic:
simp [Real.logb]

Premises used: Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
succ : ⌊logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌋₊ = Nat.log (b + 1 + 1) 0
succ₁ : ∀ (hn : n ≠ 0), ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n
⊢ ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
⊢ ⌊logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌋₊ = Nat.log (b + 1 + 1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
hn : n ≠ 0
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
hn : n ≠ 0
succ : 0 ≤ logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)
⊢ ⌊logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌋₊ = Nat.log (b + 1 + 1) n

Tactic:
rw [← Nat.cast_inj (R := ℤ), Int.natCast_floor_eq_floor, floor_logb_natCast (by simp),
    Int.log_natCast]

Premises used: Int.natCast_floor_eq_floor, Nat.cast_inj, Int.log_natCast, Real.floor_logb_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
hn : n ≠ 0
⊢ LT.lt (α := ℝ) 1 (↑(b + 1 + 1) : ℝ)

Tactic:
simp [Nat.cast_add_one_pos]

Premises used: Nat.cast_add_one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
hn : n ≠ 0
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)

Tactic:
exact logb_nonneg (by simp [Nat.cast_add_one_pos]) (Nat.one_le_cast.2 (by lia))

Premises used: Iff.mpr, Nat.one_le_cast, Real.logb_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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
succ₁ : ∀ (b : ℕ), ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n
⊢ ⌈logb (↑b : ℝ) (↑n : ℝ)⌉₊ = Nat.clog b n

Tactic:
obtain _ | _ | b := b
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n : ℕ
⊢ ⌈logb (↑0 : ℝ) (↑n : ℝ)⌉₊ = Nat.clog 0 n

Tactic:
simp [Real.logb]

Premises used: Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n : ℕ
⊢ ⌈logb (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (HAdd.hAdd (α := ℕ) 0 1) n

Tactic:
simp [Real.logb]

Premises used: Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
succ : ⌈logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌉₊ = Nat.clog (b + 1 + 1) 0
succ₁ : ∀ (hn : n ≠ 0), ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n
⊢ ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
⊢ ⌈logb (↑(b + 1 + 1) : ℝ) (↑0 : ℝ)⌉₊ = Nat.clog (b + 1 + 1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n b : ℕ
hn : n ≠ 0
succ : 0 ≤ logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)
⊢ ⌈logb (↑(b + 1 + 1) : ℝ) (↑n : ℝ)⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
rw [← Nat.cast_inj (R := ℤ), Int.natCast_ceil_eq_ceil, ceil_logb_natCast (by simp),
    Int.clog_natCast]

Premises used: Nat.cast_inj, Real.ceil_logb_natCast, Int.natCast_ceil_eq_ceil, Int.clog_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℕ
apply : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑⌊logb (↑b : ℝ) (↑a : ℝ)⌋ : ℝ)
⊢ (↑(Nat.log b a) : ℝ) ≤ logb (↑b : ℝ) (↑a : ℝ)

Tactic:
apply le_trans _ (Int.floor_le ((b : ℝ).logb a))

Premises used: Nat.cast, Real.logb, Int.floor_le, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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) : ℤ) : ℝ)
rw₂ rw₃ : LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑(Nat.log b a) : ℝ)
⊢ LE.le (α := ℝ) (↑(Nat.log b a) : ℝ) (↑⌊logb (↑b : ℝ) (↑a : ℝ)⌋ : ℝ)

Tactic:
rw [Real.floor_logb_natCast (Nat.cast_nonneg a), Int.log_natCast, Int.cast_natCast]

Premises used: Int.cast_natCast, Nat.cast_nonneg, Int.log_natCast, Real.floor_logb_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n : ℕ
⊢ Eq (α := ℝ) (↑n.log2 : ℝ) (↑(Nat.log 2 n) : ℝ)

Tactic:
mod_cast Nat.log2_eq_log_two

Premises used: cast, Nat.log2_eq_log_two, Nat.cast_inj._simp_1, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n : ℕ
⊢ (↑(Nat.log 2 n) : ℝ) ≤ logb 2 (↑n : ℝ)

Tactic:
natLog_le_logb _ _

Premises used: Real.natLog_le_logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
n : ℕ
⊢ (↑n.log2 : ℝ) ≤ logb 2 (↑n : ℝ)

Tactic:
calc (Nat.log2 n : ℝ) = Nat.log 2 n := mod_cast Nat.log2_eq_log_two
  _ ≤ Real.logb 2 n := natLog_le_logb _ _

Premises used: Nat.cast, Real.logb, Real.natLog_le_logb, Nat.log2_eq_log_two, Nat.log2, Nat.log, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
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
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
simp_rw [logb, div_eq_zero_iff, log_eq_zero]

Premises used: Real.log_eq_zero, Real.logb, div_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
⊢ Tendsto (logb b) (𝓝[≠] 0) atBot

Tactic:
tendsto_log_nhdsNE_zero.atBot_div_const (log_pos hb)

Premises used: Real.log_pos, Real.logb, Filter.Tendsto.atBot_div_const, Real.tendsto_log_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb₀ : 0 < b
hb : b < 1
⊢ Tendsto (logb b) (𝓝[≠] 0) atTop

Tactic:
tendsto_log_nhdsNE_zero.atBot_mul_const_of_neg (inv_lt_zero.2 (log_neg hb₀ hb))

Premises used: Iff.mpr, DivInvMonoid.div', Filter.Tendsto.atBot_mul_const_of_neg, Real.logb, inv_lt_zero, Real.log_neg, Real.tendsto_log_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
⊢ Tendsto (logb b) (𝓝[>] 0) atBot

Tactic:
tendsto_log_nhdsGT_zero.atBot_div_const (log_pos hb)

Premises used: Real.log_pos, Real.tendsto_log_nhdsGT_zero, Real.logb, Filter.Tendsto.atBot_div_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb₀ : 0 < b
hb : b < 1
⊢ Tendsto (logb b) (𝓝[>] 0) atTop

Tactic:
tendsto_log_nhdsGT_zero.atBot_mul_const_of_neg (inv_lt_zero.2 (log_neg hb₀ hb))

Premises used: Iff.mpr, DivInvMonoid.div', Real.tendsto_log_nhdsGT_zero, Filter.Tendsto.atBot_mul_const_of_neg, Real.logb, inv_lt_zero, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
inr :
  ∀
    (this :
      ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop)
    (hb₀ : ¬0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
wlog : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop

Tactic:
wlog hb₀ : 0 < b generalizing b
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ -b ≠ -1 ∧ -b ≠ 0 ∧ -b ≠ 1

Tactic:
simp [hb, neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : -b ≤ 0 → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : -b ≤ 0 → -1 < b → b < 0 → b < 1 → b - 0 + (-b - 0) = 0
linarith₆ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
linarith₇ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₈ : -b ≤ 0 → -1 < b → 0 < b → b < 1 → 0 - b + (b - 0) = 0
linarith₉ : -b ≤ 0 → -1 < b → 0 < b → 1 < b → -1 + (1 - b) + (b - 0) = 0
⊢ 0 < -b

Tactic:
linarith +splitNe
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ ∀ (x : ℝ), |logb (-b) x| = |logb b x|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop

Tactic:
exact (this (b := -b) (by simp [hb, neg_eq_iff_eq_neg]) (by linarith +splitNe)).congr (by simp)

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
inr :
  ∀
    (this :
      ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
        Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop)
    (hb₁ : ¬1 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
wlog :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop

Tactic:
wlog hb₁ : 1 < b generalizing b
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ b⁻¹ ≠ -1 ∧ b⁻¹ ≠ 0 ∧ b⁻¹ ≠ 1

Tactic:
simp [hb, inv_eq_iff_eq_inv, inv_neg]

Premises used: inv_neg, inv_eq_iff_eq_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ 0 < b⁻¹

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : 1 ≤ b → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : 1 ≤ b → -1 < b → b < 0 → b < 1 → b - 0 + (0 - b) = 0
linarith₆ : 1 ≤ b → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
linarith₇ : 1 ≤ b → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₈ : 1 ≤ b → -1 < b → 0 < b → b < 1 → b - 1 + (1 - b) = 0
linarith₉ : 1 ≤ b → -1 < b → 0 < b → 1 < b → 1 - b + (b - 1) = 0
⊢ b < 1

Tactic:
linarith +splitNe
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ ∀ (x : ℝ), |logb b⁻¹ x| = |logb b x|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop

Tactic:
exact (this (b := b⁻¹) (by simp [hb, inv_eq_iff_eq_inv, inv_neg]) (by simpa)
      ((one_lt_inv₀ hb₀).2 (by linarith +splitNe))).congr (by simp)

Premises used: Iff.mpr, Filter.Tendsto.congr, one_lt_inv₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop

Tactic:
(tendsto_logb_atTop hb₁).congr' ?_

Premises used: Real.tendsto_logb_atTop, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
refine : logb b =ᶠ[atTop] fun (x : ℝ) ↦ |logb b x|
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop

Tactic:
refine (tendsto_logb_atTop hb₁).congr' ?_

Premises used: Real.tendsto_logb_atTop, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
h : ∀ (x : ℝ) (hx₁ : 1 ≤ x), logb b x = |logb b x|
⊢ logb b =ᶠ[atTop] fun (x : ℝ) ↦ |logb b x|

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx₁

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
h : 0 ≤ logb b x
⊢ logb b x = |logb b x|

Tactic:
rw [abs_of_nonneg]

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ 0 ≤ logb b x

Tactic:
logb_nonneg hb₁ hx₁

Premises used: Real.logb_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ 0 ≤ logb b x

Tactic:
exact logb_nonneg hb₁ hx₁

Premises used: Real.logb_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
⊢ ContinuousOn (logb b) {0}ᶜ

Tactic:
continuousOn_log.div_const _

Premises used: ContinuousOn.div_const, Real.continuousOn_log, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
⊢ Continuous (Y := ℝ) fun (x : { x : ℝ // x ≠ 0 }) ↦ logb b (↑x : ℝ)

Tactic:
continuous_log.div_const _

Premises used: Real.continuous_log, Continuous.div_const, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
⊢ Continuous (Y := ℝ) fun (x : { x : ℝ // 0 < x }) ↦ logb b (↑x : ℝ)

Tactic:
continuous_log'.div_const _

Premises used: Real.continuous_log', Continuous.div_const, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hx : x ≠ 0
⊢ ContinuousAt (logb b) x

Tactic:
(continuousAt_log hx).div_const _

Premises used: ContinuousAt.div_const, Real.logb, Real.continuousAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x ↔ x ≠ 0

Tactic:
⟨?_, continuousAt_logb⟩

Premises used: Iff.intro, Real.continuousAt_logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
refine : ContinuousAt (logb b) x → x ≠ 0
⊢ ContinuousAt (logb b) x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_logb⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : b < 1
⊢ False

Tactic:
not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atTop, Real.tendsto_logb_nhdsNE_zero_of_base_lt_one, ContinuousAt.tendsto, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : b < 1
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atTop, Real.tendsto_logb_nhdsNE_zero_of_base_lt_one, ContinuousAt.tendsto, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : 1 < b
⊢ False

Tactic:
not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atBot, ContinuousAt.tendsto, Filter.Tendsto.mono_left, inf_le_left, Real.tendsto_logb_nhdsNE_zero