awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|

Tactic:
exact le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
⊢ log (rexp x) = x

Tactic:
exp_injective <| exp_log (exp_pos x)

Premises used: Real.exp_log, Real.exp_injective, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ log ∘ rexp = id

Tactic:
funext log_exp

Premises used: Real.log_exp, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
pos : ∀ (hx0 : x ≤ 0), rexp 1 * x ≤ rexp x
neg : ∀ (hx0 : ¬x ≤ 0), rexp 1 * x ≤ rexp x
⊢ rexp 1 * x ≤ rexp x

Tactic:
by_cases hx0 : x ≤ 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Tactic:
apply le_trans (mul_nonpos_of_nonneg_of_nonpos (exp_pos 1).le hx0) (exp_nonneg x)

Premises used: LT.lt.le, Real.exp_nonneg, mul_nonpos_of_nonneg_of_nonpos, OfNat.ofNat, Real.exp_pos, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : ¬x ≤ 0
⊢ log x + 1 ≤ rexp (log x)

Tactic:
have h := add_one_le_exp (log x)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : ¬x ≤ 0
h : log x + 1 ≤ rexp (log x)
neg : ∀ (h : rexp (log x + 1) ≤ rexp (rexp (log x))), rexp 1 * x ≤ rexp x
neg₁ : ∀ (h : rexp (log x) * rexp 1 ≤ rexp (rexp (log x))), rexp 1 * x ≤ rexp x
neg₂ : ∀ (h : x * rexp 1 ≤ rexp x), rexp 1 * x ≤ rexp x
neg₃ neg₄ neg₅ neg₆ : ∀ (h : rexp 1 * x ≤ rexp x), rexp 1 * x ≤ rexp x
⊢ rexp 1 * x ≤ rexp x

Tactic:
rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_ge hx0), mul_comm] at h

Premises used: lt_of_not_ge, Real.exp_log, Real.exp_le_exp, mul_comm, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
pos : ∀ (hx0 : x < 0), 2 * x ≤ rexp x
neg : ∀ (hx0 : ¬x < 0), 2 * x ≤ rexp x
⊢ 2 * x ≤ rexp x

Tactic:
by_cases hx0 : x < 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : x < 0
⊢ LE.le (α := ℝ) 0 2

Tactic:
simp only [Nat.ofNat_nonneg]

Premises used: Nat.ofNat_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : x < 0
⊢ 2 * x ≤ rexp x

Tactic:
exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by simp only [Nat.ofNat_nonneg]) hx0.le)
      (exp_nonneg x)

Premises used: LT.lt.le, Real.exp_nonneg, mul_nonpos_of_nonneg_of_nonpos, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : ¬x < 0
apply : 2 ≤ rexp 1
⊢ 2 * x ≤ rexp x

Tactic:
apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp

Premises used: Real.exp_one_mul_le_exp, le_of_not_gt, mul_le_mul_of_nonneg_right, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : ¬x < 0
⊢ HAdd.hAdd (α := ℝ) 1 1 ≤ rexp 1

Tactic:
have := Real.add_one_le_exp 1
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx0 : ¬x < 0
this : HAdd.hAdd (α := ℝ) 1 1 ≤ rexp 1
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : 2 ≤ rexp 1), 2 ≤ rexp 1
⊢ 2 ≤ rexp 1

Tactic:
rwa [one_add_one_eq_two] at this

Premises used: one_add_one_eq_two
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ SurjOn log (Ioi 0) univ

Tactic:
fun x _ => ⟨exp x, exp_pos x, log_exp x⟩

Premises used: Real.log_exp, Set.Mem, setOf, Set.SurjOn, Real.exp, Set.Subset, And.intro, Exists.intro, Set.image, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Surjective log

Tactic:
fun x => ⟨exp x, log_exp x⟩

Premises used: Real.log_exp, Real.exp, Exists.intro, Function.Surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ range log = univ

Tactic:
log_surjective.range_eq

Premises used: Function.Surjective.range_eq, Real.log_surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ log 0 = 0

Tactic:
dif_pos rfl

Premises used: dif_pos, Real.log, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
rw : 1 = rexp 0
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ rexp (log 1) = rexp 0

Tactic:
rw [exp_log zero_lt_one, exp_zero]

Premises used: Real.exp_log, zero_lt_one, Real.exp_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
inl : log (0 / 0) = 0
inr : ∀ (hx : x ≠ 0), log (x / x) = 0
⊢ log (x / x) = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ log (0 / 0) = 0

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x ≠ 0
⊢ log (x / x) = 0

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
pos : ∀ (h : x = 0), log |x| = log x
neg : ∀ (h : ¬x = 0), log |x| = log x
⊢ log |x| = log x

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : x = 0
⊢ log |x| = log x

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : ¬x = 0
neg : rexp (log |x|) = rexp (log x)
neg₁ : rexp (log |x|) = |x|
neg₂ : |(|x|)| = |x|
neg₃ neg₄ : |x| = |x|
⊢ log |x| = log x

Tactic:
rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]

Premises used: Iff.mpr, Real.exp_eq_exp, LT.lt.ne', abs_pos, abs_abs, Real.exp_log_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
rw : log (-x) = log |x|
rw₁ : log |(-x)| = log |x|
rw₂ rw₃ : log |x| = log |x|
⊢ log (-x) = log x

Tactic:
rw [← log_abs x, ← log_abs (-x), abs_neg]

Premises used: abs_neg, Real.log_abs, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
rw : (rexp (log x) - rexp (-log x)) / 2 = (x - x⁻¹) / 2
rw₁ : (rexp (log x) - (rexp (log x))⁻¹) / 2 = (x - x⁻¹) / 2
rw₂ rw₃ : (x - x⁻¹) / 2 = (x - x⁻¹) / 2
⊢ sinh (log x) = (x - x⁻¹) / 2

Tactic:
rw [sinh_eq, exp_neg, exp_log hx]

Premises used: Real.sinh_eq, Real.exp_log, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
rw : (rexp (log x) + rexp (-log x)) / 2 = (x + x⁻¹) / 2
rw₁ : (rexp (log x) + (rexp (log x))⁻¹) / 2 = (x + x⁻¹) / 2
rw₂ rw₃ : (x + x⁻¹) / 2 = (x + x⁻¹) / 2
⊢ cosh (log x) = (x + x⁻¹) / 2

Tactic:
rw [cosh_eq, exp_neg, exp_log hx]

Premises used: Real.exp_log, Real.cosh_eq, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
rw : log (rexp x) = x
rw₁ rw₂ : x = x
⊢ log (-rexp x) = x

Tactic:
rw [log_neg_eq_log, log_exp]

Premises used: Real.log_exp, Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
rw : |x * y| = rexp (log x + log y)
rw₁ : |x * y| = rexp (log x) * rexp (log y)
rw₂ : |x * y| = |x| * rexp (log y)
rw₃ : |x * y| = |x| * |y|
rw₄ rw₅ : |x| * |y| = |x| * |y|
⊢ rexp (log (x * y)) = rexp (log x + log y)

Tactic:
rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]

Premises used: abs_mul, mul_ne_zero, Real.exp_log_eq_abs, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
rw : |x / y| = rexp (log x - log y)
rw₁ : |x / y| = rexp (log x) / rexp (log y)
rw₂ : |x / y| = |x| / rexp (log y)
rw₃ : |x / y| = |x| / |y|
rw₄ rw₅ : |x| / |y| = |x| / |y|
⊢ rexp (log (x / y)) = rexp (log x - log y)

Tactic:
rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]

Premises used: abs_div, div_ne_zero, Real.exp_sub, Real.exp_log_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
pos : ∀ (hx : x = 0), log x⁻¹ = -log x
neg : ∀ (hx : ¬x = 0), log x⁻¹ = -log x
⊢ log x⁻¹ = -log x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : ¬x = 0
neg : rexp (log x⁻¹) = rexp (-log x)
neg₁ : |x⁻¹| = rexp (-log x)
neg₂ : |x⁻¹| = (rexp (log x))⁻¹
neg₃ : |x⁻¹| = |x|⁻¹
neg₄ neg₅ : |x|⁻¹ = |x|⁻¹
⊢ log x⁻¹ = -log x

Tactic:
rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]

Premises used: Real.exp_eq_exp, abs_inv, inv_ne_zero, Real.exp_neg, Real.exp_log_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : 0 < x
h₁ : 0 < y
rw : rexp (log x) ≤ rexp (log y) ↔ x ≤ y
rw₁ : x ≤ rexp (log y) ↔ x ≤ y
rw₂ rw₃ : x ≤ y ↔ x ≤ y
⊢ log x ≤ log y ↔ x ≤ y

Tactic:
rw [← exp_le_exp, exp_log h, exp_log h₁]

Premises used: Real.exp_log, Real.exp_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hx : 0 < x
hxy : x ≤ y
⊢ log x ≤ log y

Tactic:
(log_le_log_iff hx (hx.trans_le hxy)).2 hxy

Premises used: Iff.mpr, Real.log_le_log_iff, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hx : 0 < x
h : x < y
rwa : rexp (log x) < rexp (log y)
rwa₁ : x < rexp (log y)
rwa₂ rwa₃ rwa₄ rwa₅ : x < y
⊢ log x < log y

Tactic:
rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]

Premises used: lt_trans, Real.exp_log, Real.exp_lt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hx : 0 < x
hy : 0 < y
rw : rexp (log x) < rexp (log y) ↔ x < y
rw₁ : x < rexp (log y) ↔ x < y
rw₂ rw₃ : x < y ↔ x < y
⊢ log x < log y ↔ x < y

Tactic:
rw [← exp_lt_exp, exp_log hx, exp_log hy]

Premises used: Real.exp_log, Real.exp_lt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x) ≤ rexp y ↔ x ≤ rexp y
rw₁ rw₂ : x ≤ rexp y ↔ x ≤ rexp y
⊢ log x ≤ y ↔ x ≤ rexp y

Tactic:
rw [← exp_le_exp, exp_log hx]

Premises used: Real.exp_log, Real.exp_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x) < rexp y ↔ x < rexp y
rw₁ rw₂ : x < rexp y ↔ x < rexp y
⊢ log x < y ↔ x < rexp y

Tactic:
rw [← exp_lt_exp, exp_log hx]

Premises used: Real.exp_log, Real.exp_lt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hy : 0 < y
rw : rexp x ≤ rexp (log y) ↔ rexp x ≤ y
rw₁ rw₂ : rexp x ≤ y ↔ rexp x ≤ y
⊢ x ≤ log y ↔ rexp x ≤ y

Tactic:
rw [← exp_le_exp, exp_log hy]

Premises used: Real.exp_log, Real.exp_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
hy : 0 < y
rw : rexp x < rexp (log y) ↔ rexp x < y
rw₁ rw₂ : rexp x < y ↔ rexp x < y
⊢ x < log y ↔ rexp x < y

Tactic:
rw [← exp_lt_exp, exp_log hy]

Premises used: Real.exp_log, Real.exp_lt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x ≤ y
inl : ∀ (hx : x ≤ 0), x ≤ rexp y
inr : ∀ (hx : 0 < x), x ≤ rexp y
⊢ x ≤ rexp y

Tactic:
rcases le_or_gt x 0 with hx | hx

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x ≤ y
hx : x ≤ 0
⊢ x ≤ rexp y

Tactic:
hx.trans <| exp_nonneg y

Premises used: Real.exp_nonneg, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x ≤ y
hx : x ≤ 0
⊢ x ≤ rexp y

Tactic:
exact hx.trans <| exp_nonneg y

Premises used: Real.exp_nonneg, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x ≤ y
hx : 0 < x
⊢ x ≤ rexp y

Tactic:
(log_le_iff_le_exp hx).mp h

Premises used: Real.log_le_iff_le_exp, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x ≤ y
hx : 0 < x
⊢ x ≤ rexp y

Tactic:
exact (log_le_iff_le_exp hx).mp h

Premises used: Real.log_le_iff_le_exp, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x < y
inl : ∀ (hx : x ≤ 0), x < rexp y
inr : ∀ (hx : 0 < x), x < rexp y
⊢ x < rexp y

Tactic:
rcases le_or_gt x 0 with hx | hx

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x < y
hx : x ≤ 0
⊢ x < rexp y

Tactic:
hx.trans_lt <| exp_pos y

Premises used: LE.le.trans_lt, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x < y
hx : x ≤ 0
⊢ x < rexp y

Tactic:
exact hx.trans_lt <| exp_pos y

Premises used: LE.le.trans_lt, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y

Tactic:
(log_lt_iff_lt_exp hx).mp h

Premises used: Real.log_lt_iff_lt_exp, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y

Tactic:
exact (log_lt_iff_lt_exp hx).mp h

Premises used: Real.log_lt_iff_lt_exp, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), 0 < log 0 ↔ LT.lt (α := ℝ) 1 0
inr : ∀ (hx : 0 < x), 0 < log x ↔ 1 < x
⊢ 0 < log x ↔ 1 < x

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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
hx : LE.le (α := ℝ) 0 0
⊢ 0 < log 0 ↔ LT.lt (α := ℝ) 1 0

Tactic:
simp [zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
inr : log 1 < log x ↔ 1 < x
⊢ 0 < log x ↔ 1 < x

Tactic:
rw [← log_one]

Premises used: Real.log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x

Tactic:
log_lt_log_iff zero_lt_one hx

Premises used: zero_lt_one, Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x

Tactic:
exact log_lt_log_iff zero_lt_one hx

Premises used: zero_lt_one, Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 1 < x
⊢ 0 < log x

Tactic:
(log_pos_iff (lt_trans zero_lt_one hx).le).2 hx

Premises used: Iff.mpr, lt_trans, Real.log_pos_iff, LT.lt.le, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < -1
rw : 0 < log (-x)
⊢ 0 < log x

Tactic:
rw [← neg_neg x, log_neg_eq_log]

Premises used: Real.log_neg_eq_log, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < -1
linarith : -x ≤ 1 → x - -1 + (-x - 1) = 0
⊢ 1 < -x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < -1
⊢ 1 < -x

Tactic:
have : 1 < -x := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)

Tactic:
log_pos this

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)

Tactic:
exact log_pos this

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : 0 < x
rw : log x < log 1 ↔ x < 1
⊢ log x < 0 ↔ x < 1

Tactic:
rw [← log_one]

Premises used: Real.log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1

Tactic:
log_lt_log_iff h zero_lt_one

Premises used: zero_lt_one, Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1

Tactic:
exact log_lt_log_iff h zero_lt_one

Premises used: zero_lt_one, Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : 0 < x
h1 : x < 1
⊢ log x < 0

Tactic:
(log_neg_iff h0).2 h1

Premises used: Iff.mpr, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
rw : log (-x) < 0
⊢ log x < 0

Tactic:
rw [← neg_neg x, log_neg_eq_log]

Premises used: Real.log_neg_eq_log, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
linarith : -x ≤ 0 → x - 0 + (-x - 0) = 0
⊢ 0 < -x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ 0 < -x

Tactic:
have h0' : 0 < -x := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
linarith : 1 ≤ -x → -1 - x + (1 - -x) = 0
⊢ -x < 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ -x < 1

Tactic:
have h1' : -x < 1 := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
h1' : -x < 1
⊢ log (-x) < 0

Tactic:
log_neg h0' h1'

Premises used: Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
h1' : -x < 1
⊢ log (-x) < 0

Tactic:
exact log_neg h0' h1'

Premises used: Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
rw : ¬log x < 0 ↔ 1 ≤ x
rw₁ : ¬x < 1 ↔ 1 ≤ x
rw₂ rw₃ : 1 ≤ x ↔ 1 ≤ x
⊢ 0 ≤ log x ↔ 1 ≤ x

Tactic:
rw [← not_lt, log_neg_iff hx, not_lt]

Premises used: not_lt, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log x

Tactic:
(log_nonneg_iff (zero_lt_one.trans_le hx)).2 hx

Premises used: Iff.mpr, zero_lt_one, LT.lt.trans_le, Real.log_nonneg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ 0 ↔ LE.le (α := ℝ) 0 1
inr : ∀ (hx : 0 < x), log x ≤ 0 ↔ x ≤ 1
⊢ log 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.Basic
Goal:
hx : LE.le (α := ℝ) 0 0
⊢ log 0 ≤ 0 ↔ LE.le (α := ℝ) 0 1

Tactic:
simp [zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
inr : ¬0 < log x ↔ x ≤ 1
inr₁ : ¬1 < x ↔ x ≤ 1
inr₂ inr₃ : x ≤ 1 ↔ x ≤ 1
⊢ log x ≤ 0 ↔ x ≤ 1

Tactic:
rw [← not_lt, log_pos_iff hx.le, not_lt]

Premises used: Real.log_pos_iff, LT.lt.le, not_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
h'x : x ≤ 1
⊢ log x ≤ 0

Tactic:
(log_nonpos_iff hx).2 h'x

Premises used: Iff.mpr, Real.log_nonpos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
hn : n = 0
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
hn : ¬n = 0
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
hn : ¬n = 0
this : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
log_nonneg this

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
hn : ¬n = 0
this : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
exact log_nonneg this

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
if : ∀ (hn : n = 0), 0 ≤ log (↑n : ℝ)
if₁ : ∀ (hn : ¬n = 0), 0 ≤ log (↑n : ℝ)
if₂ : ∀ (hn : n = 0), 0 ≤ log (↑n : ℝ)
if₃ if₄ : ∀ (hn : ¬n = 0), 0 ≤ log (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
if hn : n = 0 then
    simp [hn]
  else
    have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
    exact log_nonneg this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
rw : 0 ≤ log (↑n : ℝ)
⊢ 0 ≤ log (-(↑n : ℝ))

Tactic:
rw [← log_neg_eq_log, neg_neg]

Premises used: Real.log_neg_eq_log, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
log_natCast_nonneg _

Premises used: Real.log_natCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
exact log_natCast_nonneg _

Premises used: Real.log_natCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : 0 < n
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
have : (1 : ℝ) ≤ n := mod_cast hn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : 0 < n
this : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
log_nonneg this

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : 0 < n
this : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
exact log_nonneg this

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : 0 = n
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
simp [hn.symm]

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : n < 0
⊢ 0 < -n

Tactic:
rw [← neg_zero, ← lt_neg] at hn

Premises used: lt_neg, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : 0 < -n
⊢ LE.le (α := ℝ) 1 (-(↑n : ℝ))

Tactic:
mod_cast hn

Premises used: Int.cast, congrArg, Int.cast_neg._simp_1, cast, LE.le, Int.cast_le._simp_1, Nat.cast, LT.lt, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.cast_one, Neg.neg, Int.cast_one, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : 0 < -n
⊢ LE.le (α := ℝ) 1 (-(↑n : ℝ))

Tactic:
exact mod_cast hn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : n < 0
⊢ LE.le (α := ℝ) 1 (-(↑n : ℝ))

Tactic:
have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : n < 0
this : LE.le (α := ℝ) 1 (-(↑n : ℝ))
inr : 0 ≤ log (-(↑n : ℝ))
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
rw [← log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : n < 0
this : LE.le (α := ℝ) 1 (-(↑n : ℝ))
⊢ 0 ≤ log (-(↑n : ℝ))

Tactic:
log_nonneg this

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : n < 0
this : LE.le (α := ℝ) 1 (-(↑n : ℝ))
⊢ 0 ≤ log (-(↑n : ℝ))

Tactic:
exact log_nonneg this

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
hn : 0 = n ∨ n < 0
inr : ∀ (hn : 0 = n), 0 ≤ log (↑n : ℝ)
inr₁ : ∀ (hn : n < 0), 0 ≤ log (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)

Tactic:
cases hn with
      | inl hn => simp [hn.symm]
      | inr hn =>
          have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
          rw [← log_neg_eq_log]
          exact log_nonneg this

Premises used: Real.log_neg_eq_log, Or.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℤ
⊢ 0 < n ∨ 0 = n ∨ n < 0

Tactic:
cases lt_trichotomy 0 n with
  | inl hn =>
      have : (1 : ℝ) ≤ n := mod_cast hn
      exact log_nonneg this
  | inr hn =>
      cases hn with
      | inl hn => simp [hn.symm]
      | inr hn =>
          have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
          rw [← log_neg_eq_log]
          exact log_nonneg this

Premises used: Real.log_neg_eq_log, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ StrictMonoOn log (Ioi 0)

Tactic:
fun _ hx _ _ hxy => log_lt_log hx hxy

Premises used: Real.log_lt_log, StrictMonoOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
rw : log |y| < log |x|
⊢ log y < log x

Tactic:
rw [← log_abs y, ← log_abs x]

Premises used: Real.log_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|

Tactic:
log_lt_log (abs_pos.2 hy.ne) ?_

Premises used: Iff.mpr, Real.log_lt_log, abs_pos, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
refine : |y| < |x|
⊢ log |y| < log |x|

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

Premises used: Iff.mpr, Real.log_lt_log, abs_pos, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
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.Basic
Goal:
⊢ InjOn log (Ioi 0)

Tactic:
strictMonoOn_log.injOn

Premises used: StrictMonoOn.injOn, Real.strictMonoOn_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
rwa : Membership.mem (γ := Set ℝ) (Ioi 0) 1
⊢ log x ≠ 0

Tactic:
rwa [← log_one, log_injOn_pos.ne_iff hx1]

Premises used: Real.log_one, Set.InjOn.ne_iff, Real.log_injOn_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) 1

Tactic:
mem_Ioi.mpr zero_lt_one

Premises used: Iff.mpr, Set.mem_Ioi, zero_lt_one