awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) univ x
h : 0 < b ^ x
⊢ Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x)

Tactic:
simp only [Right.neg_neg_iff, Set.mem_Iio]

Premises used: Set.mem_Iio, Right.neg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
⊢ 0 < b ^ x

Tactic:
apply rpow_pos_of_pos b_pos

Premises used: Real.rpow_pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) univ x
h : logb b (b ^ x) = x
h₁ h₂ : x = x
⊢ logb b (-b ^ x) = x

Tactic:
rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]

Premises used: Real.logb_neg_eq_logb, Real.logb_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
linarith : b ≤ 0 → -1 + (1 - b) + (b - 0) = 0
⊢ 0 < b

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
linarith : b = 1 → 1 - b + (b - 1) = 0
⊢ b ≠ 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
rw : log x / log b ≤ logb b y ↔ x ≤ y
rw₁ : log x / log b ≤ log y / log b ↔ x ≤ y
rw₂ : log x ≤ log y ↔ x ≤ y
rw₃ rw₄ : x ≤ y ↔ x ≤ y
⊢ logb b x ≤ logb b y ↔ x ≤ y

Tactic:
rw [logb, logb, div_le_div_iff_of_pos_right (log_pos hb), log_le_log_iff h h₁]

Premises used: Real.log_pos, div_le_div_iff_of_pos_right, Real.logb, Real.log_le_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
h : 0 < x
hxy : x ≤ y
linarith : y ≤ 0 → 0 - x + (x - y) + (y - 0) = 0
⊢ 0 < y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
rw : log x < log y
⊢ logb b x < logb b y

Tactic:
rw [logb, logb, div_lt_div_iff_of_pos_right (log_pos hb)]

Premises used: div_lt_div_iff_of_pos_right, Real.log_pos, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y

Tactic:
log_lt_log hx hxy

Premises used: Real.log_lt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y

Tactic:
exact log_lt_log hx hxy

Premises used: Real.log_lt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
rw : log x < log y ↔ x < y
⊢ logb b x < logb b y ↔ x < y

Tactic:
rw [logb, logb, div_lt_div_iff_of_pos_right (log_pos hb)]

Premises used: div_lt_div_iff_of_pos_right, Real.log_pos, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Tactic:
log_lt_log_iff hx hy

Premises used: Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Tactic:
exact log_lt_log_iff hx hy

Premises used: Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
rw : b ^ logb b x ≤ b ^ y ↔ x ≤ b ^ y
rw₁ rw₂ : x ≤ b ^ y ↔ x ≤ b ^ y
⊢ logb b x ≤ y ↔ x ≤ b ^ y

Tactic:
rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]

Premises used: _private.0.Real.b_pos, Real.rpow_le_rpow_left_iff, Real.rpow_logb, _private.0.Real.b_ne_one'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
rw : b ^ logb b x < b ^ y ↔ x < b ^ y
rw₁ rw₂ : x < b ^ y ↔ x < b ^ y
⊢ logb b x < y ↔ x < b ^ y

Tactic:
rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]

Premises used: Real.rpow_lt_rpow_left_iff, _private.0.Real.b_pos, Real.rpow_logb, _private.0.Real.b_ne_one'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hy : 0 < y
rw : b ^ x ≤ b ^ logb b y ↔ b ^ x ≤ y
rw₁ rw₂ : b ^ x ≤ y ↔ b ^ x ≤ y
⊢ x ≤ logb b y ↔ b ^ x ≤ y

Tactic:
rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]

Premises used: _private.0.Real.b_pos, Real.rpow_le_rpow_left_iff, Real.rpow_logb, _private.0.Real.b_ne_one'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hb : 1 < b
hy : 0 < y
rw : b ^ x < b ^ logb b y ↔ b ^ x < y
rw₁ rw₂ : b ^ x < y ↔ b ^ x < y
⊢ x < logb b y ↔ b ^ x < y

Tactic:
rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]

Premises used: Real.rpow_lt_rpow_left_iff, _private.0.Real.b_pos, Real.rpow_logb, _private.0.Real.b_ne_one'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw : logb b 1 < logb b x ↔ 1 < x
⊢ 0 < logb b x ↔ 1 < x

Tactic:
rw [← @logb_one b]

Premises used: Real.logb_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw rw₁ : 1 < x ↔ 1 < x
⊢ logb b 1 < logb b x ↔ 1 < x

Tactic:
rw [logb_lt_logb_iff hb zero_lt_one hx]

Premises used: Real.logb_lt_logb_iff, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx rw : 1 < x
⊢ 0 < logb b x

Tactic:
rw [logb_pos_iff hb (lt_trans zero_lt_one hx)]

Premises used: lt_trans, zero_lt_one, Real.logb_pos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 1 < x
⊢ 1 < x

Tactic:
hx
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 1 < x
⊢ 1 < x

Tactic:
exact hx
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
h : 0 < x
rw : logb b x < logb b 1 ↔ x < 1
rw₁ : ℝ
⊢ logb b x < 0 ↔ x < 1

Tactic:
rw [← logb_one]

Premises used: Real.logb_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < logb b 1 ↔ x < 1

Tactic:
logb_lt_logb_iff hb h zero_lt_one

Premises used: Real.logb_lt_logb_iff, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
h0 : 0 < x
h1 : x < 1
⊢ logb b x < 0

Tactic:
(logb_neg_iff hb h0).2 h1

Premises used: Iff.mpr, Real.logb_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw : ¬logb b x < 0 ↔ 1 ≤ x
rw₁ : ¬x < 1 ↔ 1 ≤ x
rw₂ rw₃ : 1 ≤ x ↔ 1 ≤ x
⊢ 0 ≤ logb b x ↔ 1 ≤ x

Tactic:
rw [← not_lt, logb_neg_iff hb hx, not_lt]

Premises used: not_lt, Real.logb_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 1 ≤ x
⊢ 0 ≤ logb b x

Tactic:
(logb_nonneg_iff hb (zero_lt_one.trans_le hx)).2 hx

Premises used: Iff.mpr, zero_lt_one, LT.lt.trans_le, Real.logb_nonneg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw : ¬0 < logb b x ↔ x ≤ 1
rw₁ : ¬1 < x ↔ x ≤ 1
rw₂ rw₃ : x ≤ 1 ↔ x ≤ 1
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
rw [← not_lt, logb_pos_iff hb hx, not_lt]

Premises used: not_lt, Real.logb_pos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), logb b 0 ≤ 0 ↔ LE.le (α := ℝ) 0 1
inr : ∀ (hx : 0 < x), logb b x ≤ 0 ↔ x ≤ 1
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
hx : LE.le (α := ℝ) 0 0
⊢ logb b 0 ≤ 0 ↔ LE.le (α := ℝ) 0 1

Tactic:
simp [zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx_1 : 0 ≤ x
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
logb_nonpos_iff hb hx

Premises used: Real.logb_nonpos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx_1 : 0 ≤ x
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
exact logb_nonpos_iff hb hx

Premises used: Real.logb_nonpos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx : 0 ≤ x
h'x : x ≤ 1
⊢ logb b x ≤ 0

Tactic:
(logb_nonpos_iff' hb hx).2 h'x

Premises used: Iff.mpr, Real.logb_nonpos_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
⊢ StrictMonoOn (logb b) (Ioi 0)

Tactic:
fun _ hx _ _ hxy =>
  logb_lt_logb hb hx hxy

Premises used: Real.logb_lt_logb, StrictMonoOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
rw : logb b |y| < logb b |x|
⊢ logb b y < logb b x

Tactic:
rw [← logb_abs b y, ← logb_abs b x]

Premises used: Real.logb_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |y| < logb b |x|

Tactic:
logb_lt_logb hb (abs_pos.2 hy.ne) ?_

Premises used: Iff.mpr, abs_pos, Real.logb_lt_logb, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
refine : |y| < |x|
⊢ logb b |y| < logb b |x|

Tactic:
refine logb_lt_logb hb (abs_pos.2 hy.ne) ?_

Premises used: Iff.mpr, abs_pos, Real.logb_lt_logb, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
rwa : -y < |x|
rwa₁ : -y < -x
rwa₂ rwa₃ rwa₄ rwa₅ : x < y
⊢ |y| < |x|

Tactic:
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, abs_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
⊢ InjOn (logb b) (Ioi 0)

Tactic:
(strictMonoOn_logb hb).injOn

Premises used: StrictMonoOn.injOn, Real.strictMonoOn_logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
h₁ : 0 < x
h₂ : logb b x = 0
⊢ x = 1

Tactic:
logb_injOn_pos hb (Set.mem_Ioi.2 h₁) (Set.mem_Ioi.2 zero_lt_one) (h₂.trans Real.logb_one.symm)

Premises used: Iff.mpr, Real.logb_one, Set.mem_Ioi, Real.logb_injOn_pos, zero_lt_one, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
hb : 1 < b
hx_pos : 0 < x
hx : x ≠ 1
⊢ logb b x ≠ 0

Tactic:
mt (eq_one_of_pos_of_logb_eq_zero hb hx_pos) hx

Premises used: mt, Real.eq_one_of_pos_of_logb_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
⊢ Tendsto (logb b) atTop atTop

Tactic:
Tendsto.atTop_div_const (log_pos hb) tendsto_log_atTop

Premises used: Real.log_pos, Real.logb, Filter.Tendsto.atTop_div_const, Real.tendsto_log_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_lt_one : b < 1
linarith : b = 1 → b - 1 + -(b - 1) = 0
⊢ b ≠ 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
rw : log x / log b ≤ logb b y ↔ y ≤ x
rw₁ : log x / log b ≤ log y / log b ↔ y ≤ x
rw₂ : log y ≤ log x ↔ y ≤ x
rw₃ rw₄ : y ≤ x ↔ y ≤ x
⊢ logb b x ≤ logb b y ↔ y ≤ x

Tactic:
rw [logb, logb, div_le_div_right_of_neg (log_neg b_pos b_lt_one), log_le_log_iff h₁ h]

Premises used: div_le_div_right_of_neg, Real.logb, Real.log_le_log_iff, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
rw : log x < log y
⊢ logb b y < logb b x

Tactic:
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]

Premises used: div_lt_div_right_of_neg, Real.logb, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ log x < log y

Tactic:
log_lt_log hx hxy

Premises used: Real.log_lt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ log x < log y

Tactic:
exact log_lt_log hx hxy

Premises used: Real.log_lt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
rw : log y < log x ↔ y < x
⊢ logb b x < logb b y ↔ y < x

Tactic:
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]

Premises used: div_lt_div_right_of_neg, Real.logb, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ log y < log x ↔ y < x

Tactic:
log_lt_log_iff hy hx

Premises used: Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ log y < log x ↔ y < x

Tactic:
exact log_lt_log_iff hy hx

Premises used: Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : b ^ y ≤ b ^ logb b x ↔ b ^ y ≤ x
rw₁ rw₂ : b ^ y ≤ x ↔ b ^ y ≤ x
⊢ logb b x ≤ y ↔ b ^ y ≤ x

Tactic:
rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]

Premises used: Real.rpow_logb, Real.rpow_le_rpow_left_iff_of_base_lt_one, _private.0.Real.b_ne_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : b ^ y < b ^ logb b x ↔ b ^ y < x
rw₁ rw₂ : b ^ y < x ↔ b ^ y < x
⊢ logb b x < y ↔ b ^ y < x

Tactic:
rw [← rpow_lt_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]

Premises used: Real.rpow_logb, _private.0.Real.b_ne_one, Real.rpow_lt_rpow_left_iff_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
rw : b ^ logb b y ≤ b ^ x ↔ y ≤ b ^ x
rw₁ rw₂ : y ≤ b ^ x ↔ y ≤ b ^ x
⊢ x ≤ logb b y ↔ y ≤ b ^ x

Tactic:
rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hy]

Premises used: Real.rpow_logb, Real.rpow_le_rpow_left_iff_of_base_lt_one, _private.0.Real.b_ne_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
rw : b ^ logb b y < b ^ x ↔ y < b ^ x
rw₁ rw₂ : y < b ^ x ↔ y < b ^ x
⊢ x < logb b y ↔ y < b ^ x

Tactic:
rw [← rpow_lt_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hy]

Premises used: Real.rpow_logb, _private.0.Real.b_ne_one, Real.rpow_lt_rpow_left_iff_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
rw : logb b 1 < logb b x ↔ x < 1
rw₁ rw₂ : x < 1 ↔ x < 1
⊢ 0 < logb b x ↔ x < 1

Tactic:
rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one zero_lt_one hx]

Premises used: Real.logb_one, Real.logb_lt_logb_iff_of_base_lt_one, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' rw : x < 1
⊢ 0 < logb b x

Tactic:
rw [logb_pos_iff_of_base_lt_one b_pos b_lt_one hx]

Premises used: Real.logb_pos_iff_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ x < 1

Tactic:
hx'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ x < 1

Tactic:
exact hx'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
rw : logb b x < logb b 1 ↔ 1 < x
rw₁ rw₂ : 1 < x ↔ 1 < x
⊢ logb b x < 0 ↔ 1 < x

Tactic:
rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one h zero_lt_one]

Premises used: Real.logb_one, Real.logb_lt_logb_iff_of_base_lt_one, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h1 : 1 < x
⊢ logb b x < 0

Tactic:
(logb_neg_iff_of_base_lt_one b_pos b_lt_one (lt_trans zero_lt_one h1)).2 h1

Premises used: Iff.mpr, lt_trans, Real.logb_neg_iff_of_base_lt_one, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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
rw₂ rw₃ : x ≤ 1 ↔ x ≤ 1
⊢ 0 ≤ logb b x ↔ x ≤ 1

Tactic:
rw [← not_lt, logb_neg_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]

Premises used: Real.logb_neg_iff_of_base_lt_one, not_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' rw : x ≤ 1
⊢ 0 ≤ logb b x

Tactic:
rw [logb_nonneg_iff_of_base_lt_one b_pos b_lt_one hx]

Premises used: Real.logb_nonneg_iff_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ x ≤ 1

Tactic:
hx'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ x ≤ 1

Tactic:
exact hx'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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
rw₂ rw₃ : 1 ≤ x ↔ 1 ≤ x
⊢ logb b x ≤ 0 ↔ 1 ≤ x

Tactic:
rw [← not_lt, logb_pos_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]

Premises used: not_lt, Real.logb_pos_iff_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ StrictAntiOn (logb b) (Ioi 0)

Tactic:
fun _ hx _ _ hxy =>
  logb_lt_logb_of_base_lt_one b_pos b_lt_one hx hxy

Premises used: StrictAntiOn, Real.logb_lt_logb_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
rw : logb b |x| < logb b |y|
⊢ logb b x < logb b y

Tactic:
rw [← logb_abs b y, ← logb_abs b x]

Premises used: Real.logb_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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|

Tactic:
logb_lt_logb_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) ?_

Premises used: Iff.mpr, Real.logb_lt_logb_of_base_lt_one, abs_pos, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
refine : |y| < |x|
⊢ logb b |x| < logb b |y|

Tactic:
refine logb_lt_logb_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) ?_

Premises used: Iff.mpr, Real.logb_lt_logb_of_base_lt_one, abs_pos, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
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|
rwa₁ : -y < -x
rwa₂ rwa₃ rwa₄ rwa₅ : x < y
⊢ |y| < |x|

Tactic:
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, abs_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ InjOn (logb b) (Ioi 0)

Tactic:
(strictAntiOn_logb_of_base_lt_one b_pos b_lt_one).injOn

Premises used: StrictAntiOn.injOn, Real.strictAntiOn_logb_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h₁ : 0 < x
h₂ : logb b x = 0
⊢ x = 1

Tactic:
logb_injOn_pos_of_base_lt_one b_pos b_lt_one (Set.mem_Ioi.2 h₁) (Set.mem_Ioi.2 zero_lt_one)
    (h₂.trans Real.logb_one.symm)

Premises used: Iff.mpr, Real.logb_one, Set.mem_Ioi, zero_lt_one, Real.logb_injOn_pos_of_base_lt_one, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx_pos : 0 < x
hx : x ≠ 1
⊢ logb b x ≠ 0

Tactic:
mt (eq_one_of_pos_of_logb_eq_zero_of_base_lt_one b_pos b_lt_one hx_pos) hx

Premises used: Real.eq_one_of_pos_of_logb_eq_zero_of_base_lt_one, mt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
rw : ∀ (b_1 : ℝ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → logb b a ≤ b_1
⊢ Tendsto (logb b) atTop atBot

Tactic:
rw [tendsto_atTop_atBot]

Premises used: Filter.tendsto_atTop_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
h : ∀ (a : ℝ), max 1 (b ^ e) ≤ a → logb b a ≤ e
⊢ ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → logb b a ≤ e

Tactic:
use 1 ⊔ b ^ e
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
h : 1 ≤ a → b ^ e ≤ a → logb b a ≤ e
⊢ max 1 (b ^ e) ≤ a → logb b a ≤ e

Tactic:
simp only [and_imp, sup_le_iff]

Premises used: and_imp, sup_le_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
h : b ^ e ≤ a → b ^ e ≤ a
h₁ : 0 < a
⊢ b ^ e ≤ a → logb b a ≤ e

Tactic:
rw [logb_le_iff_le_rpow_of_base_lt_one b_pos b_lt_one]

Premises used: Real.logb_le_iff_le_rpow_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
h h₁ h₂ : b ^ e ≤ a → b ^ e ≤ a
⊢ b ^ e ≤ a → b ^ e ≤ a

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a

Tactic:
lt_of_lt_of_le zero_lt_one ha

Premises used: zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a

Tactic:
exact lt_of_lt_of_le zero_lt_one ha

Premises used: zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr : 0 ≤ r
inl : ∀ (hr : LE.le (α := ℝ) 0 0), ⌊logb (↑b : ℝ) 0⌋ = Int.log (R := ℝ) b 0
inr : ∀ (hr : 0 < r), ⌊logb (↑b : ℝ) r⌋ = Int.log b r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log 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.floor (α := ℝ) 0 = Int.log (R := ℝ) b 0
inl₁ : Int.floor (α := ℝ) 0 = 0
inl₂ inl₃ : Eq (α := ℤ) 0 0
⊢ ⌊logb (↑b : ℝ) 0⌋ = Int.log (R := ℝ) b 0

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

Premises used: Int.floor_zero, Int.log_zero_right, Real.logb_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℕ
r : ℝ
hr_1 : 0 ≤ r
hr : 0 < r
pos : ∀ (hb : 1 < b), ⌊logb (↑b : ℝ) r⌋ = Int.log b r
neg : ∀ (hb : ¬1 < b), ⌊logb (↑b : ℝ) r⌋ = Int.log b r
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log 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
⊢ LT.lt (α := ℝ) 1 (↑b : ℝ)

Tactic:
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
-- 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.log b r
pos₁ : Int.log b r ≤ ⌊logb (↑b : ℝ) r⌋
⊢ ⌊logb (↑b : ℝ) r⌋ = Int.log 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 : HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌊logb (↑b : ℝ) r⌋ : ℝ) ≤ r
⊢ ⌊logb (↑b : ℝ) r⌋ ≤ Int.log b r

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

Premises used: Int.zpow_le_iff_le_log, Nat.cast, 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 : ℝ) (↑⌊logb (↑b : ℝ) r⌋ : ℝ) ≤ r

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

Premises used: le_of_le_of_eq, Real.rpow_logb, LT.lt.ne', zero_lt_one, LT.lt.trans
-- 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)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌊logb (↑b : ℝ) r⌋ : ℝ) ≤ r

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

Premises used: le_of_le_of_eq, Real.rpow_logb, LT.lt.ne', zero_lt_one, LT.lt.trans
-- 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.floor_le _)

Premises used: LT.lt.le, Int.floor_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.floor_le _)

Premises used: LT.lt.le, Int.floor_le, Real.rpow_le_rpow_of_exponent_le