awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) 1

Tactic:
exact mem_Ioi.mpr zero_lt_one

Premises used: Iff.mpr, Set.mem_Ioi, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0

Tactic:
have h : log x ≠ 0 := by
    rwa [← log_one, log_injOn_pos.ne_iff hx1]
    exact mem_Ioi.mpr zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
linarith : x - 1 ≤ log x → x - 1 - log x + (log x + 1 - rexp (log x)) + (rexp (log x) - x) = 0
⊢ log x < x - 1

Tactic:
linarith [add_one_lt_exp h, exp_log hx1]

Premises used: Real.exp_log, Real.add_one_lt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h₁ : 0 < x
h₂ : log x = 0
⊢ x = 1

Tactic:
log_injOn_pos (Set.mem_Ioi.2 h₁) (Set.mem_Ioi.2 zero_lt_one) (h₂.trans Real.log_one.symm)

Premises used: Iff.mpr, Set.mem_Ioi, Real.log_one, zero_lt_one, Eq.symm, Eq.trans, Real.log_injOn_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx_pos : 0 < x
hx : x ≠ 1
⊢ log x ≠ 0

Tactic:
mt (eq_one_of_pos_of_log_eq_zero hx_pos) hx

Premises used: mt, Real.eq_one_of_pos_of_log_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
mp : log x = 0 → x = 0 ∨ x = 1 ∨ x = -1
mpr : x = 0 ∨ x = 1 ∨ x = -1 → log x = 0
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log x = 0
mp : ∀ (x_lt_zero : x < 0), x = 0 ∨ x = 1 ∨ x = -1
mp₁ : ∀ (h : log 0 = 0), Eq (α := ℝ) 0 0 ∨ Eq (α := ℝ) 0 1 ∨ Eq (α := ℝ) 0 (-1)
mp₂ : ∀ (x_gt_zero : 0 < x), x = 0 ∨ x = 1 ∨ x = -1
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
Or.inr (Or.inr (neg_eq_iff_eq_neg.mp ?_))

Premises used: neg_eq_iff_eq_neg, Iff.mp, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log x = 0
x_lt_zero : x < 0
mp : -x = 1
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
refine Or.inr (Or.inr (neg_eq_iff_eq_neg.mp ?_))

Premises used: neg_eq_iff_eq_neg, Iff.mp, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ log (-x) = 0

Tactic:
rw [← log_neg_eq_log x] at h

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log x = 0
x_lt_zero : x < 0
h₁ : log (-x) = 0
⊢ x < 0

Tactic:
rw [← log_neg_eq_log x] at h

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1

Tactic:
eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h

Premises used: Iff.mpr, neg_pos, Real.eq_one_of_pos_of_log_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1

Tactic:
exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h

Premises used: Iff.mpr, neg_pos, Real.eq_one_of_pos_of_log_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
h : log 0 = 0
⊢ Eq (α := ℝ) 0 0 ∨ Eq (α := ℝ) 0 1 ∨ Eq (α := ℝ) 0 (-1)

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
h : log 0 = 0
⊢ Eq (α := ℝ) 0 0 ∨ Eq (α := ℝ) 0 1 ∨ Eq (α := ℝ) 0 (-1)

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))

Premises used: Real.eq_one_of_pos_of_log_eq_zero, Or.inl, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))

Premises used: Real.eq_one_of_pos_of_log_eq_zero, Or.inl, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ log 0 = 0

Tactic:
simp only [log_one, log_zero, log_neg_eq_log]

Premises used: Real.log_neg_eq_log, Real.log_one, Real.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ log 1 = 0

Tactic:
simp only [log_one, log_zero, log_neg_eq_log]

Premises used: Real.log_neg_eq_log, Real.log_one, Real.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ log (-1) = 0

Tactic:
simp only [log_one, log_zero, log_neg_eq_log]

Premises used: Real.log_neg_eq_log, Real.log_one, Real.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
⊢ log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
simpa only [not_or] using log_eq_zero.not

Premises used: Iff.not, Real.log_eq_zero, not_or
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
⊢ log (HPow.hPow (β := ℕ) x 0) = (↑0 : ℝ) * log x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
n : ℕ
ih : log (x ^ n) = (↑n : ℝ) * log x
succ :
  ∀ (ih : log (HPow.hPow (α := ℝ) 0 n) = (↑n : ℝ) * log 0), log (HPow.hPow (α := ℝ) 0 (n + 1)) = (↑(n + 1) : ℝ) * log 0
succ₁ : ∀ (hx : x ≠ 0), log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
ih : log (HPow.hPow (α := ℝ) 0 n) = (↑n : ℝ) * log 0
⊢ log (HPow.hPow (α := ℝ) 0 (n + 1)) = (↑(n + 1) : ℝ) * log 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
n : ℕ
ih : log (x ^ n) = (↑n : ℝ) * log x
hx : x ≠ 0
succ : log (x ^ n * x) = (↑(n + 1) : ℝ) * log x
succ₁ : log (x ^ n) + log x = (↑(n + 1) : ℝ) * log x
succ₂ : (↑n : ℝ) * log x + log x = (↑(n + 1) : ℝ) * log x
succ₃ : (↑n : ℝ) * log x + log x = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * log x
succ₄ : (↑n : ℝ) * log x + log x = (↑n : ℝ) * log x + 1 * log x
succ₅ succ₆ : (↑n : ℝ) * log x + log x = (↑n : ℝ) * log x + log x
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x

Tactic:
rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]

Premises used: add_mul, Nat.cast_succ, pow_succ, pow_ne_zero, Real.log_mul, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
n : ℕ
zero : log (HPow.hPow (β := ℕ) x 0) = (↑0 : ℝ) * log x
succ : ∀ (n : ℕ) (ih : log (x ^ n) = (↑n : ℝ) * log x), log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
⊢ log (x ^ n) = (↑n : ℝ) * log x

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rcases eq_or_ne x 0 with (rfl | hx)
    · simp
    · rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]

Premises used: add_mul, Nat.cast_succ, pow_succ, eq_or_ne, OfNat.ofNat, one_mul, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
n : ℤ
ofNat : ∀ (a : ℕ), log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x
negSucc : ∀ (a : ℕ), log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
⊢ log (x ^ n) = (↑n : ℝ) * log x

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
a : ℕ
ofNat : log (HPow.hPow (β := ℤ) x (↑a : ℤ)) = (↑(↑a : ℤ) : ℝ) * log x
ofNat₁ : log (x ^ a) = (↑(↑a : ℤ) : ℝ) * log x
ofNat₂ : (↑a : ℝ) * log x = (↑(↑a : ℤ) : ℝ) * log x
ofNat₃ ofNat₄ : (↑a : ℝ) * log x = (↑a : ℝ) * log x
⊢ log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x

Tactic:
rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]

Premises used: zpow_natCast, Int.cast_natCast, Int.ofNat_eq_natCast, Real.log_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
a : ℕ
negSucc : log (x ^ (a + 1))⁻¹ = (↑(Int.negSucc a) : ℝ) * log x
negSucc₁ : -log (x ^ (a + 1)) = (↑(Int.negSucc a) : ℝ) * log x
negSucc₂ : -((↑(a + 1) : ℝ) * log x) = (↑(Int.negSucc a) : ℝ) * log x
negSucc₃ : -((↑(a + 1) : ℝ) * log x) = -(↑(a + 1) : ℝ) * log x
negSucc₄ : -(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x) = -HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x
negSucc₅ negSucc₆ : -HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x = -HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x
⊢ log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x

Tactic:
rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]

Premises used: zpow_negSucc, Int.cast_negSucc, Real.log_pow, neg_mul_eq_neg_mul, Real.log_inv, Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
rw : Ne (α := ℝ) 2 0
⊢ log √x = log x / 2

Tactic:
rw [eq_div_iff, mul_comm, ← Nat.cast_two, ← log_pow, sq_sqrt hx]

Premises used: Real.sq_sqrt, mul_comm, Real.log_pow, eq_div_iff, Nat.cast_two
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
⊢ Ne (α := ℝ) 2 0

Tactic:
two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
⊢ Ne (α := ℝ) 2 0

Tactic:
exact two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
rw : log x + 1 ≤ x
⊢ log x ≤ x - 1

Tactic:
rw [le_sub_iff_add_le]

Premises used: le_sub_iff_add_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ rexp (log x)

Tactic:
add_one_le_exp (log x)

Premises used: Real.log, Real.add_one_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
h : x = rexp (log x)
⊢ log x + 1 ≤ x

Tactic:
convert! add_one_le_exp (log x)

Premises used: Real.log, Real.add_one_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
h h₁ : x = x
⊢ x = rexp (log x)

Tactic:
rw [exp_log hx]

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
⊢ 1 - x⁻¹ ≤ log x

Tactic:
simpa [add_comm] using log_le_sub_one_of_pos (inv_pos.2 hx)

Premises used: Iff.mpr, inv_pos, add_comm, Real.log_le_sub_one_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ 0
inr : ∀ (hx : 0 < x), log x ≤ x
⊢ log x ≤ x

Tactic:
obtain rfl | hx := hx.eq_or_lt

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

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
linarith : x < x - 1 → -1 + (x - (x - 1)) = 0
⊢ x - 1 ≤ x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ log x ≤ x

Tactic:
exact (log_le_sub_one_of_pos hx).trans (by linarith)

Premises used: LE.le.trans, Real.log_le_sub_one_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
rw : log x⁻¹ ≤ x⁻¹
⊢ -x⁻¹ ≤ log x

Tactic:
rw [neg_le, ← log_inv]

Premises used: neg_le, Real.log_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log x⁻¹ ≤ x⁻¹

Tactic:
log_le_self <| inv_nonneg.2 hx

Premises used: Iff.mpr, Real.log_le_self, inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log x⁻¹ ≤ x⁻¹

Tactic:
exact log_le_self <| inv_nonneg.2 hx

Premises used: Iff.mpr, Real.log_le_self, inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < 1 / x

Tactic:
simpa only [one_div, inv_pos] using h1

Premises used: inv_pos, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < 1 / x

Tactic:
have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ log (1 / x) ≤ 1 / x - 1

Tactic:
replace := log_le_sub_one_of_pos this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
linarith :
  1 / x ≤ log (1 / x) →
    -1 + (1 * log (1 / x) - (1 * (1 / x) - HMul.hMul (α := ℝ) 1 1)) + (1 * (1 / x) - 1 * log (1 / x)) = 0
⊢ log (1 / x) < 1 / x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ log (1 / x) < 1 / x

Tactic:
replace : log (1 / x) < 1 / x := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ -log x * x < 1

Tactic:
rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff₀ h1] at this

Premises used: lt_div_iff₀, Real.log_one, Real.log_div, LT.lt.ne', one_ne_zero, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x * x

Tactic:
mul_nonneg ?_ h1.le

Premises used: mul_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
refine : 0 ≤ -log x
⊢ 0 ≤ -log x * x

Tactic:
refine mul_nonneg ?_ h1.le

Premises used: mul_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
rw : 0 ≤ log x⁻¹
⊢ 0 ≤ -log x

Tactic:
rw [← log_inv]

Premises used: Real.log_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
hx : 1 ≤ x⁻¹
⊢ 0 ≤ log x⁻¹

Tactic:
apply log_nonneg

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
hx : x ≤ 1
⊢ 1 ≤ x⁻¹

Tactic:
rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]

Premises used: le_inv_comm₀, inv_one, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1

Tactic:
h2
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1

Tactic:
exact h2
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x * x

Tactic:
have aux : 0 ≤ -log x * x := by
    refine mul_nonneg ?_ h1.le
    rw [← log_inv]
    apply log_nonneg
    rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]
    exact h2
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Tactic:
rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this

Premises used: abs_neg, abs_of_nonneg, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
this₁ : |log x * x| < 1
⊢ 0 ≤ -log x * x

Tactic:
rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this

Premises used: abs_neg, abs_of_nonneg, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (rexp x)) atTop atTop

Tactic:
simpa only [log_exp] using tendsto_id

Premises used: Real.log_exp, Filter.tendsto_id
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Tendsto log (𝓝[>] 0) atBot

Tactic:
simpa [← tendsto_comp_exp_atBot] using tendsto_id

Premises used: Filter.tendsto_id, Real.tendsto_comp_exp_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Tendsto log (𝓝[≠] 0) atBot

Tactic:
simpa [comp_def] using tendsto_log_nhdsGT_zero.comp tendsto_abs_nhdsNE_zero

Premises used: tendsto_abs_nhdsNE_zero, Real.tendsto_log_nhdsGT_zero, Function.comp_def, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Tendsto log (𝓝[<] 0) atBot

Tactic:
tendsto_log_nhdsNE_zero.mono_left <| nhdsWithin_mono _ fun _ h ↦ ne_of_lt h

Premises used: Filter.Tendsto.mono_left, Real.tendsto_log_nhdsNE_zero, ne_of_lt, nhdsWithin_mono
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
simp : Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦ log (↑x : ℝ)
⊢ ContinuousOn log {0}ᶜ

Tactic:
simp +unfoldPartialApp only [continuousOn_iff_continuous_restrict,
    restrict]

Premises used: continuousOn_iff_continuous_restrict, Set.restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : (↑{0}ᶜ : Type)
rw :
  ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |(↑x : ℝ)| ⋯) :
    ℝ)
| log (↑x : ℝ)

Tactic:
rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]

Premises used: Real.log_of_ne_zero, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
conv :
  Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦
    (expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |(↑x : ℝ)| ⋯)
⊢ Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦ log (↑x : ℝ)

Tactic:
conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]

Premises used: Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦
    (expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |(↑x : ℝ)| ⋯)

Tactic:
expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)

Premises used: OrderIso.continuous, continuous_subtype_val, Continuous.comp, Continuous.subtype_mk, OrderIso.symm, Continuous.norm, Real.expOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦
    (expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |(↑x : ℝ)| ⋯)

Tactic:
exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)

Premises used: OrderIso.continuous, continuous_subtype_val, Continuous.comp, Continuous.subtype_mk, OrderIso.symm, Continuous.norm, Real.expOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : { x : ℝ // x ≠ 0 }) ↦ log (↑x : ℝ)

Tactic:
continuousOn_iff_continuous_restrict.1 <| continuousOn_log.mono fun _ => id

Premises used: Set.Mem, Real.continuousOn_log, setOf, id, Real.log, continuousOn_iff_continuous_restrict, Set.singleton, Iff.mp, ContinuousOn.mono, Set.restrict, Not
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : { x : ℝ // 0 < x }) ↦ log (↑x : ℝ)

Tactic:
continuousOn_iff_continuous_restrict.1 <| continuousOn_log.mono fun _ hx => ne_of_gt hx

Premises used: Set.Mem, Real.continuousOn_log, ne_of_gt, Real.log, continuousOn_iff_continuous_restrict, Iff.mp, ContinuousOn.mono, Set.restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x ≠ 0
⊢ ContinuousAt log x

Tactic:
(continuousOn_log x hx).continuousAt <| isOpen_compl_singleton.mem_nhds hx

Premises used: Real.continuousOn_log, isOpen_compl_singleton, IsOpen.mem_nhds, ContinuousWithinAt.continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0

Tactic:
⟨?_, continuousAt_log⟩

Premises used: Iff.intro, Real.continuousAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
refine : ContinuousAt log x → x ≠ 0
⊢ ContinuousAt log x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_log⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
h : ContinuousAt log 0
⊢ False

Tactic:
not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsNE_zero _ <|
    h.tendsto.mono_left nhdsWithin_le_nhds

Premises used: not_tendsto_nhds_of_tendsto_atBot, nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left, Real.tendsto_log_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
h : ContinuousAt log 0
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsNE_zero _ <|
    h.tendsto.mono_left nhdsWithin_le_nhds

Premises used: not_tendsto_nhds_of_tendsto_atBot, nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left, Real.tendsto_log_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
h : ∀ (x : ℝ), Membership.mem (γ := List ℝ) [] x → x ≠ 0
⊢ log (List.prod []) = sum (List.map (fun (x : ℝ) ↦ log x) [])

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
a : ℝ
l : List ℝ
ih : ∀ (h : ∀ x ∈ l, x ≠ 0), log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ∀ x ∈ a :: l, x ≠ 0
⊢ log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)

Tactic:
simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]

Premises used: List.map_cons, forall_eq_or_imp, ne_eq, List.sum_cons, forall_const, List.mem_cons, not_false_eq_true, List.prod_cons, or_true
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
a : ℝ
l : List ℝ
ih : ∀ (h : ∀ x ∈ l, x ≠ 0), log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ∀ x ∈ a :: l, x ≠ 0
ih₁ : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
⊢ ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0

Tactic:
simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]

Premises used: List.map_cons, forall_eq_or_imp, ne_eq, List.sum_cons, forall_const, List.mem_cons, not_false_eq_true, List.prod_cons, or_true
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
a : ℝ
l : List ℝ
ih : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
⊢ l.prod ≠ 0

Tactic:
grind [prod_ne_zero]

Premises used: List.prod_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
a : ℝ
l : List ℝ
ih : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
⊢ l.prod ≠ 0

Tactic:
have : l.prod ≠ 0 := by grind [prod_ne_zero]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
a : ℝ
l : List ℝ
ih : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
cons : log a + log l.prod = log a + sum (List.map (fun (x : ℝ) ↦ log x) l)
cons₁ : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
cons₂ cons₃ : Eq (α := ℝ) (sum (List.map (fun (x : ℝ) ↦ log x) l)) (sum (List.map (fun (x : ℝ) ↦ log x) l))
⊢ log (a * l.prod) = log a + sum (List.map (fun (x : ℝ) ↦ log x) l)

Tactic:
rw [log_mul h.1 this, add_right_inj, ih]

Premises used: And.left, add_right_inj, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
l : List ℝ
h : ∀ x ∈ l, x ≠ 0
nil :
  ∀ (h : ∀ (x : ℝ), Membership.mem (γ := List ℝ) [] x → x ≠ 0),
    log (List.prod []) = sum (List.map (fun (x : ℝ) ↦ log x) [])
cons :
  ∀ (a : ℝ) (l : List ℝ) (ih : ∀ (h : ∀ x ∈ l, x ≠ 0), log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l))
    (h : ∀ x ∈ a :: l, x ≠ 0), log (a :: l).prod = sum (List.map (fun (x : ℝ) ↦ log x) (a :: l))
⊢ log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]
    have : l.prod ≠ 0 := by grind [prod_ne_zero]
    rw [log_mul h.1 this, add_right_inj, ih]

Premises used: List.map_cons, forall_eq_or_imp, ne_eq, List.cons, List.sum_cons, forall_const, List.mem_cons, not_false_eq_true, List.prod_cons, or_true, add_right_inj, List.nil
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ ∀ x ∈ s.toList, x ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
rw : log s.toList.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)
rw₁ : Eq (α := ℝ) (List.sum (List.map (fun (x : ℝ) ↦ log x) s.toList)) (sum (Multiset.map (fun (x : ℝ) ↦ log x) s))
rw₂ rw₃ : Eq (α := ℝ) (sum (Multiset.map (fun (x : ℝ) ↦ log x) s)) (sum (Multiset.map (fun (x : ℝ) ↦ log x) s))
⊢ log s.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)

Tactic:
rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]

Premises used: Real.log_list_prod, Multiset.prod_toList, Multiset.sum_map_toList