awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
h : logb (-b) x = logb |b| x
h₁ : logb |(-b)| x = logb |b| x
⊢ logb (-b) x = logb b x
have h₂ : logb |b| x = logb |b| x
Tactic: rw [← logb_abs_base b x, ← logb_abs_base (-b) x, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
⊢ logb b (-x) = logb b x
have rw : logb b (-x) = logb b |x|
Tactic: rw [← logb_abs b x, ← logb_abs b (-x), abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
rw : logb b (-x) = logb b |x|
⊢ logb b (-x) = logb b x
have rw₁ : logb b |(-x)| = logb b |x|
Tactic: rw [← logb_abs b x, ← logb_abs b (-x), abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
rw : logb b (-x) = logb b |x|
rw₁ : logb b |(-x)| = logb b |x|
⊢ logb b (-x) = logb b x
have rw₂ : logb b |x| = logb b |x|
Tactic: rw [← logb_abs b x, ← logb_abs b (-x), abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x * y) = logb b x + logb b y
have simp_rw : log (x * y) / log b = log x / log b + log y / log b
Tactic: simp_rw [logb, log_mul hx hy, add_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
simp_rw : log (x * y) / log b = log x / log b + log y / log b
⊢ logb b (x * y) = logb b x + logb b y
have simp_rw₁ : (log x + log y) / log b = log x / log b + log y / log b
Tactic: simp_rw [logb, log_mul hx hy, add_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x / y) = logb b x - logb b y
have simp_rw : log (x / y) / log b = log x / log b - log y / log b
Tactic: simp_rw [logb, log_div hx hy, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
simp_rw : log (x / y) / log b = log x / log b - log y / log b
⊢ logb b (x / y) = logb b x - logb b y
have simp_rw₁ : (log x - log y) / log b = log x / log b - log y / log b
Tactic: simp_rw [logb, log_div hx hy, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹
have simp_rw : logb c (a * b) = logb c a + logb c b
Tactic: simp_rw [inv_logb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹
have simp_rw : logb c (a / b) = logb c a - logb c b
Tactic: simp_rw [inv_logb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹
have rw : logb (a * b) c = (logb (a * b) c)⁻¹⁻¹
Tactic: rw [← inv_logb_mul_base h₁ h₂ c, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
rw : logb (a * b) c = (logb (a * b) c)⁻¹⁻¹
⊢ logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹
have rw₁ : logb (a * b) c = logb (a * b) c
Tactic: rw [← inv_logb_mul_base h₁ h₂ c, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹
have rw : logb (a / b) c = (logb (a / b) c)⁻¹⁻¹
Tactic: rw [← inv_logb_div_base h₁ h₂ c, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
rw : logb (a / b) c = (logb (a / b) c)⁻¹⁻¹
⊢ logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹
have rw₁ : logb (a / b) c = logb (a / b) c
Tactic: rw [← inv_logb_div_base h₁ h₂ c, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ log b / log a * (log c / log b) = log c / log a
have rw : log c / log b * (log b / log a) = log c / log a
Tactic: rw [mul_comm, div_mul_div_cancel₀ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
rw : log c / log b * (log b / log a) = log c / log a
⊢ log b / log a * (log c / log b) = log c / log a
have rw₁ : log c / log a = log c / log a
Tactic: rw [mul_comm, div_mul_div_cancel₀ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : 0 < x
⊢ logb b (x ^ y) = y * logb b x
have rw : log (x ^ y) / log b = y * logb b x
Tactic: rw [logb, log_rpow hx, logb, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : 0 < x
rw : log (x ^ y) / log b = y * logb b x
⊢ logb b (x ^ y) = y * logb b x
have rw₁ : y * log x / log b = y * logb b x
Tactic: rw [logb, log_rpow hx, logb, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : 0 < x
rw : log (x ^ y) / log b = y * logb b x
rw₁ : y * log x / log b = y * logb b x
⊢ logb b (x ^ y) = y * logb b x
have rw₂ : y * log x / log b = y * (log x / log b)
Tactic: rw [logb, log_rpow hx, logb, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hx : 0 < x
rw : log (x ^ y) / log b = y * logb b x
rw₁ : y * log x / log b = y * logb b x
rw₂ : y * log x / log b = y * (log x / log b)
⊢ logb b (x ^ y) = y * logb b x
have rw₃ : y * (log x / log b) = y * (log x / log b)
Tactic: rw [logb, log_rpow hx, logb, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
k : ℕ
⊢ logb b (x ^ k) = (↑k : ℝ) * logb b x
have rw : log (x ^ k) / log b = (↑k : ℝ) * logb b x
Tactic: rw [logb, logb, log_pow, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
k : ℕ
rw : log (x ^ k) / log b = (↑k : ℝ) * logb b x
⊢ logb b (x ^ k) = (↑k : ℝ) * logb b x
have rw₁ : log (x ^ k) / log b = (↑k : ℝ) * (log x / log b)
Tactic: rw [logb, logb, log_pow, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
k : ℕ
rw : log (x ^ k) / log b = (↑k : ℝ) * logb b x
rw₁ : log (x ^ k) / log b = (↑k : ℝ) * (log x / log b)
⊢ logb b (x ^ k) = (↑k : ℝ) * logb b x
have rw₂ : (↑k : ℝ) * log x / log b = (↑k : ℝ) * (log x / log b)
Tactic: rw [logb, logb, log_pow, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
k : ℕ
rw : log (x ^ k) / log b = (↑k : ℝ) * logb b x
rw₁ : log (x ^ k) / log b = (↑k : ℝ) * (log x / log b)
rw₂ : (↑k : ℝ) * log x / log b = (↑k : ℝ) * (log x / log b)
⊢ logb b (x ^ k) = (↑k : ℝ) * logb b x
have rw₃ : (↑k : ℝ) * (log x / log b) = (↑k : ℝ) * (log x / log b)
Tactic: rw [logb, logb, log_pow, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ logb b (b ^ x) = x
have rw : log b ≠ 0
Tactic: rw [logb, div_eq_iff, log_rpow b_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x = |x|
have a : Membership.mem (γ := Set ℝ) (Ioi 0) (b ^ logb b x)
Tactic: apply log_injOn_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
a : Membership.mem (γ := Set ℝ) (Ioi 0) (b ^ logb b x)
⊢ b ^ logb b x = |x|
have a₁ : Membership.mem (γ := Set ℝ) (Ioi 0) |x|
Tactic: apply log_injOn_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
a : Membership.mem (γ := Set ℝ) (Ioi 0) (b ^ logb b x)
a₁ : Membership.mem (γ := Set ℝ) (Ioi 0) |x|
⊢ b ^ logb b x = |x|
have a₂ : log (b ^ logb b x) = log |x|
Tactic: apply log_injOn_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|
have a : log x / log b * log b = log x
Tactic: rw [log_rpow b_pos, logb, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ b ^ logb b x = x
have rw : |x| = x
Tactic: rw [rpow_logb_eq_abs b_pos b_ne_one hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ b ^ logb b x = -x
have rw : |x| = -x
Tactic: rw [rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ logb b y = x ↔ b ^ x = y
have mp : logb b y = x → b ^ x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
mp : logb b y = x → b ^ x = y
⊢ logb b y = x ↔ b ^ x = y
have mpr : b ^ x = y → logb b y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
⊢ x ∈ logb b '' Iio 0
have h : Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x) ∧ logb b (-b ^ x) = x
Tactic: use -b ^ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
⊢ Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x) ∧ logb b (-b ^ x) = x
have h : Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) univ x
h : Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x)
⊢ Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x) ∧ logb b (-b ^ x) = x
have h₁ : logb b (-b ^ x) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
⊢ Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x)
have h : 0 < b ^ x
Tactic: simp only [Right.neg_neg_iff, Set.mem_Iio]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
⊢ logb b (-b ^ x) = x
have h : logb b (b ^ x) = x
Tactic: rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b (-b ^ x) = x
have h₁ : x = x
Tactic: rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ 0 < b
have linarith : b ≤ 0 → -1 + (1 - b) + (b - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ b ≠ 1
have linarith : b = 1 → 1 - b + (b - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ x ≤ y
have rw : log x / log b ≤ 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₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
rw : log x / log b ≤ logb b y ↔ x ≤ y
⊢ logb b x ≤ logb b y ↔ x ≤ y
have rw₁ : log x / log b ≤ log y / log b ↔ x ≤ y
Tactic: rw [logb, logb, div_le_div_iff_of_pos_right (log_pos hb), log_le_log_iff h h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b x ≤ logb b y ↔ x ≤ y
have rw₂ : log x ≤ log y ↔ x ≤ y
Tactic: rw [logb, logb, div_le_div_iff_of_pos_right (log_pos hb), log_le_log_iff h h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b x ≤ logb b y ↔ x ≤ y
have rw₃ : x ≤ y ↔ x ≤ y
Tactic: rw [logb, logb, div_le_div_iff_of_pos_right (log_pos hb), log_le_log_iff h h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
h : 0 < x
hxy : x ≤ y
⊢ 0 < y
have linarith : y ≤ 0 → 0 - x + (x - y) + (y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ logb b x < logb b y
have rw : log x < log y
Tactic: rw [logb, logb, div_lt_div_iff_of_pos_right (log_pos hb)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ x < y
have rw : log x < log y ↔ x < y
Tactic: rw [logb, logb, div_lt_div_iff_of_pos_right (log_pos hb)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ y ↔ x ≤ b ^ y
have rw : b ^ logb b x ≤ b ^ y ↔ x ≤ b ^ y
Tactic: rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
rw : b ^ logb b x ≤ b ^ y ↔ x ≤ b ^ y
⊢ logb b x ≤ y ↔ x ≤ b ^ y
have rw₁ : x ≤ b ^ y ↔ x ≤ b ^ y
Tactic: rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x < y ↔ x < b ^ y
have rw : b ^ logb b x < b ^ y ↔ x < b ^ y
Tactic: rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hx : 0 < x
rw : b ^ logb b x < b ^ y ↔ x < b ^ y
⊢ logb b x < y ↔ x < b ^ y
have rw₁ : x < b ^ y ↔ x < b ^ y
Tactic: rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ x ≤ logb b y ↔ b ^ x ≤ y
have rw : b ^ x ≤ b ^ logb b y ↔ b ^ x ≤ y
Tactic: rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hy : 0 < y
rw : b ^ x ≤ b ^ logb b y ↔ b ^ x ≤ y
⊢ x ≤ logb b y ↔ b ^ x ≤ y
have rw₁ : b ^ x ≤ y ↔ b ^ x ≤ y
Tactic: rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ x < logb b y ↔ b ^ x < y
have rw : b ^ x < b ^ logb b y ↔ b ^ x < y
Tactic: rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
hb : 1 < b
hy : 0 < y
rw : b ^ x < b ^ logb b y ↔ b ^ x < y
⊢ x < logb b y ↔ b ^ x < y
have rw₁ : b ^ x < y ↔ b ^ x < y
Tactic: rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 < logb b x ↔ 1 < x
have rw : logb b 1 < logb b x ↔ 1 < x
Tactic: rw [← @logb_one b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x
have rw : 1 < x ↔ 1 < x
Tactic: rw [logb_lt_logb_iff hb zero_lt_one hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < 0 ↔ x < 1
have rw : logb b x < logb b 1 ↔ x < 1
Tactic: rw [← logb_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 ≤ logb b x ↔ 1 ≤ x
have rw : ¬logb b x < 0 ↔ 1 ≤ x
Tactic: rw [← not_lt, logb_neg_iff hb hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw : ¬logb b x < 0 ↔ 1 ≤ x
⊢ 0 ≤ logb b x ↔ 1 ≤ x
have rw₁ : ¬x < 1 ↔ 1 ≤ x
Tactic: rw [← not_lt, logb_neg_iff hb hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw : ¬logb b x < 0 ↔ 1 ≤ x
rw₁ : ¬x < 1 ↔ 1 ≤ x
⊢ 0 ≤ logb b x ↔ 1 ≤ x
have rw₂ : 1 ≤ x ↔ 1 ≤ x
Tactic: rw [← not_lt, logb_neg_iff hb hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1
have rw : ¬0 < logb b x ↔ x ≤ 1
Tactic: rw [← not_lt, logb_pos_iff hb hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw : ¬0 < logb b x ↔ x ≤ 1
⊢ logb b x ≤ 0 ↔ x ≤ 1
have rw₁ : ¬1 < x ↔ x ≤ 1
Tactic: rw [← not_lt, logb_pos_iff hb hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 < x
rw : ¬0 < logb b x ↔ x ≤ 1
rw₁ : ¬1 < x ↔ x ≤ 1
⊢ logb b x ≤ 0 ↔ x ≤ 1
have rw₂ : x ≤ 1 ↔ x ≤ 1
Tactic: rw [← not_lt, logb_pos_iff hb hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 ≤ x
⊢ logb b x ≤ 0 ↔ x ≤ 1
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), logb b 0 ≤ 0 ↔ LE.le (α := ℝ) 0 1
Tactic: rcases hx.eq_or_lt with (rfl | hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb : 1 < b
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), logb b 0 ≤ 0 ↔ LE.le (α := ℝ) 0 1
⊢ logb b x ≤ 0 ↔ x ≤ 1
have inr : ∀ (hx : 0 < x), logb b x ≤ 0 ↔ x ≤ 1
Tactic: rcases hx.eq_or_lt with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b y < logb b x
have rw : logb b |y| < logb b |x|
Tactic: rw [← logb_abs b y, ← logb_abs b x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |y| < logb b |x|
have refine : |y| < |x|
Tactic: refine logb_lt_logb hb (abs_pos.2 hy.ne) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : 1 < b
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 : ℝ
hb : 1 < b
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_lt_one : b < 1
⊢ b ≠ 1
have linarith : b = 1 → b - 1 + -(b - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ y ≤ x
have rw : log x / log b ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b x ≤ logb b y ↔ y ≤ x
have rw₁ : log x / log b ≤ log y / log b ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b x ≤ logb b y ↔ y ≤ x
have rw₂ : log y ≤ log x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b x ≤ logb b y ↔ y ≤ x
have rw₃ : y ≤ x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ logb b y < logb b x
have rw : log x < log y
Tactic: rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ y < x
have rw : log y < log x ↔ y < x
Tactic: rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ y ↔ b ^ y ≤ x
have rw : b ^ y ≤ b ^ logb b x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b x ≤ y ↔ b ^ y ≤ x
have rw₁ : b ^ y ≤ x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x < y ↔ b ^ y < x
have rw : b ^ y < b ^ logb b x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ logb b x < y ↔ b ^ y < x
have rw₁ : b ^ y < x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x ≤ logb b y ↔ y ≤ b ^ x
have rw : b ^ logb b y ≤ b ^ x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ x ≤ logb b y ↔ y ≤ b ^ x
have rw₁ : y ≤ b ^ x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x < logb b y ↔ y < b ^ x
have rw : b ^ logb b y < b ^ x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
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
⊢ x < logb b y ↔ y < b ^ x
have rw₁ : y < b ^ x ↔ 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]
-- 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 1 < 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]