awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hy : 0 < y
⊢ x ≤ log y ↔ rexp x ≤ y
have rw : rexp x ≤ rexp (log y) ↔ rexp x ≤ y
Tactic: rw [← exp_le_exp, exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : rexp x ≤ rexp (log y) ↔ rexp x ≤ y
⊢ x ≤ log y ↔ rexp x ≤ y
have rw₁ : rexp x ≤ y ↔ rexp x ≤ y
Tactic: rw [← exp_le_exp, exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hy : 0 < y
⊢ x < log y ↔ rexp x < y
have rw : rexp x < rexp (log y) ↔ rexp x < y
Tactic: rw [← exp_lt_exp, exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : rexp x < rexp (log y) ↔ rexp x < y
⊢ x < log y ↔ rexp x < y
have rw₁ : rexp x < y ↔ rexp x < y
Tactic: rw [← exp_lt_exp, exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
h : log x ≤ y
⊢ x ≤ rexp y
have inl : ∀ (hx : x ≤ 0), x ≤ rexp y
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
h : log x ≤ y
inl : ∀ (hx : x ≤ 0), x ≤ rexp y
⊢ x ≤ rexp y
have inr : ∀ (hx : 0 < x), x ≤ rexp y
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
h : log x < y
⊢ x < rexp y
have inl : ∀ (hx : x ≤ 0), x < rexp y
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
h : log x < y
inl : ∀ (hx : x ≤ 0), x < rexp y
⊢ x < rexp y
have inr : ∀ (hx : 0 < x), x < rexp y
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 < log x ↔ 1 < x
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), 0 < log 0 ↔ LT.lt (α := ℝ) 1 0
Tactic: rcases hx.eq_or_lt with (rfl | hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), 0 < log 0 ↔ LT.lt (α := ℝ) 1 0
⊢ 0 < log x ↔ 1 < x
have inr : ∀ (hx : 0 < x), 0 < log x ↔ 1 < x
Tactic: rcases hx.eq_or_lt with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ 0 < log x ↔ 1 < x
have inr : log 1 < log x ↔ 1 < x
Tactic: rw [← log_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x < -1
⊢ 0 < log x
have rw : 0 < log (-x)
Tactic: rw [← neg_neg x, log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x < -1
⊢ 1 < -x
have linarith : -x ≤ 1 → x - -1 + (-x - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
hx : x < -1
⊢ 0 < log (-x)
have this : 1 < -x
Tactic: have : 1 < -x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : 0 < x
⊢ log x < 0 ↔ x < 1
have rw : log x < log 1 ↔ x < 1
Tactic: rw [← log_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log x < 0
have rw : log (-x) < 0
Tactic: rw [← neg_neg x, log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ 0 < -x
have linarith : -x ≤ 0 → x - 0 + (-x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (-x) < 0
have h0' : 0 < -x
Tactic: have h0' : 0 < -x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ -x < 1
have linarith : 1 ≤ -x → -1 - x + (1 - -x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ log (-x) < 0
have h1' : -x < 1
Tactic: have h1' : -x < 1 := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ 0 ≤ log x ↔ 1 ≤ x
have rw : ¬log x < 0 ↔ 1 ≤ x
Tactic: rw [← not_lt, log_neg_iff hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
rw : ¬log x < 0 ↔ 1 ≤ x
⊢ 0 ≤ log x ↔ 1 ≤ x
have rw₁ : ¬x < 1 ↔ 1 ≤ x
Tactic: rw [← not_lt, log_neg_iff hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
rw : ¬log x < 0 ↔ 1 ≤ x
rw₁ : ¬x < 1 ↔ 1 ≤ x
⊢ 0 ≤ log x ↔ 1 ≤ x
have rw₂ : 1 ≤ x ↔ 1 ≤ x
Tactic: rw [← not_lt, log_neg_iff hx, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log x ≤ 0 ↔ x ≤ 1
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 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.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ 0 ↔ LE.le (α := ℝ) 0 1
⊢ log x ≤ 0 ↔ x ≤ 1
have inr : ∀ (hx : 0 < x), log x ≤ 0 ↔ x ≤ 1
Tactic: rcases hx.eq_or_lt with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
have inr : ¬0 < log x ↔ x ≤ 1
Tactic: rw [← not_lt, log_pos_iff hx.le, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
inr : ¬0 < log x ↔ x ≤ 1
⊢ log x ≤ 0 ↔ x ≤ 1
have inr₁ : ¬1 < x ↔ x ≤ 1
Tactic: rw [← not_lt, log_pos_iff hx.le, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
inr : ¬0 < log x ↔ x ≤ 1
inr₁ : ¬1 < x ↔ x ≤ 1
⊢ log x ≤ 0 ↔ x ≤ 1
have inr₂ : x ≤ 1 ↔ x ≤ 1
Tactic: rw [← not_lt, log_pos_iff hx.le, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log (↑n : ℝ)
have this : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
⊢ 0 ≤ log (↑n : ℝ)
have if : ∀ (hn : n = 0), 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
if : ∀ (hn : n = 0), 0 ≤ log (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)
have if₁ : ∀ (hn : ¬n = 0), 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
⊢ 0 ≤ log (-(↑n : ℝ))
have rw : 0 ≤ log (↑n : ℝ)
Tactic: rw [← log_neg_eq_log, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
n : ℤ
hn : 0 < n
⊢ 0 ≤ log (↑n : ℝ)
have this : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: have : (1 : ℝ) ≤ n := mod_cast hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
n : ℤ
hn : n < 0
⊢ LE.le (α := ℝ) 1 (-(↑n : ℝ))
have hn₁ : 0 < -n
Tactic: rw [← neg_zero, ← lt_neg] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
n : ℤ
hn : n < 0
⊢ 0 ≤ log (↑n : ℝ)
have this : LE.le (α := ℝ) 1 (-(↑n : ℝ))
Tactic: have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℤ
hn : n < 0
this : LE.le (α := ℝ) 1 (-(↑n : ℝ))
⊢ 0 ≤ log (↑n : ℝ)
have inr : 0 ≤ log (-(↑n : ℝ))
Tactic: rw [← log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log (↑n : ℝ)
have inr : ∀ (hn : 0 = 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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℤ
hn : 0 = n ∨ n < 0
inr : ∀ (hn : 0 = n), 0 ≤ log (↑n : ℝ)
⊢ 0 ≤ log (↑n : ℝ)
have inr₁ : ∀ (hn : n < 0), 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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
n : ℤ
⊢ 0 ≤ log (↑n : ℝ)
have x : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log y < log x
have rw : log |y| < log |x|
Tactic: rw [← log_abs y, ← log_abs x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|
have refine : |y| < |x|
Tactic: refine log_lt_log (abs_pos.2 hy.ne) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
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.Basic (goal)
Goal:
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.Basic (goal)
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0
have rwa : Membership.mem (γ := Set ℝ) (Ioi 0) 1
Tactic: rwa [← log_one, log_injOn_pos.ne_iff hx1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x < x - 1
have h : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1
have linarith : x - 1 ≤ log x → x - 1 - log x + (log x + 1 - rexp (log x)) + (rexp (log x) - x) = 0
Tactic: linarith [add_one_lt_exp h, exp_log hx1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
have mp : log x = 0 → x = 0 ∨ x = 1 ∨ x = -1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
mp : log x = 0 → x = 0 ∨ x = 1 ∨ x = -1
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
have mpr : x = 0 ∨ x = 1 ∨ x = -1 → log x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : log x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
have mp : ∀ (x_lt_zero : x < 0), x = 0 ∨ x = 1 ∨ x = -1
Tactic: rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : log x = 0
mp : ∀ (x_lt_zero : x < 0), x = 0 ∨ x = 1 ∨ x = -1
⊢ x = 0 ∨ x = 1 ∨ x = -1
have mp₁ : ∀ (h : log 0 = 0), Eq (α := ℝ) 0 0 ∨ Eq (α := ℝ) 0 1 ∨ Eq (α := ℝ) 0 (-1)
Tactic: rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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)
⊢ x = 0 ∨ x = 1 ∨ x = -1
have mp₂ : ∀ (x_gt_zero : 0 < x), x = 0 ∨ x = 1 ∨ x = -1
Tactic: rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
have mp : -x = 1
Tactic: refine Or.inr (Or.inr (neg_eq_iff_eq_neg.mp ?_))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1
have h₁ : log (-x) = 0
Tactic: rw [← log_neg_eq_log x] at h
Cleared hypotheses: h, x_lt_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
n : ℕ
ih : log (x ^ n) = (↑n : ℝ) * log x
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ : ∀ (ih : log (HPow.hPow (α := ℝ) 0 n) = (↑n : ℝ) * log 0), log (HPow.hPow (α := ℝ) 0 (n + 1)) = (↑(n + 1) : ℝ) * log 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x, ih
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ₁ : ∀ (hx : x ≠ 0), log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
n : ℕ
ih : log (x ^ n) = (↑n : ℝ) * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ : log (x ^ n * x) = (↑(n + 1) : ℝ) * log x
Tactic: rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
n : ℕ
ih : log (x ^ n) = (↑n : ℝ) * log x
hx : x ≠ 0
succ : log (x ^ n * x) = (↑(n + 1) : ℝ) * log x
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ₁ : log (x ^ n) + log x = (↑(n + 1) : ℝ) * log x
Tactic: rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ₂ : (↑n : ℝ) * log x + log x = (↑(n + 1) : ℝ) * log x
Tactic: rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ₃ : (↑n : ℝ) * log x + log x = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * log x
Tactic: rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ₄ : (↑n : ℝ) * log x + log x = (↑n : ℝ) * log x + 1 * log x
Tactic: rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * log x
have succ₅ : (↑n : ℝ) * log x + log x = (↑n : ℝ) * log x + log x
Tactic: rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
n : ℕ
⊢ log (x ^ n) = (↑n : ℝ) * log x
have zero : log (HPow.hPow (β := ℕ) x 0) = (↑0 : ℝ) * 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
n : ℕ
zero : log (HPow.hPow (β := ℕ) x 0) = (↑0 : ℝ) * log x
⊢ log (x ^ n) = (↑n : ℝ) * log x
have succ : ∀ (n : ℕ) (ih : log (x ^ n) = (↑n : ℝ) * log x), log (x ^ (n + 1)) = (↑(n + 1) : ℝ) * 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
n : ℤ
⊢ log (x ^ n) = (↑n : ℝ) * log x
have ofNat : ∀ (a : ℕ), log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
n : ℤ
ofNat : ∀ (a : ℕ), log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x
⊢ log (x ^ n) = (↑n : ℝ) * log x
have negSucc : ∀ (a : ℕ), log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
a : ℕ
⊢ log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x
have ofNat : log (HPow.hPow (β := ℤ) x (↑a : ℤ)) = (↑(↑a : ℤ) : ℝ) * log x
Tactic: rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
a : ℕ
ofNat : log (HPow.hPow (β := ℤ) x (↑a : ℤ)) = (↑(↑a : ℤ) : ℝ) * log x
⊢ log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x
have ofNat₁ : log (x ^ a) = (↑(↑a : ℤ) : ℝ) * log x
Tactic: rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
a : ℕ
ofNat : log (HPow.hPow (β := ℤ) x (↑a : ℤ)) = (↑(↑a : ℤ) : ℝ) * log x
ofNat₁ : log (x ^ a) = (↑(↑a : ℤ) : ℝ) * log x
⊢ log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x
have ofNat₂ : (↑a : ℝ) * log x = (↑(↑a : ℤ) : ℝ) * log x
Tactic: rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ Int.ofNat a) = (↑(Int.ofNat a) : ℝ) * log x
have ofNat₃ : (↑a : ℝ) * log x = (↑a : ℝ) * log x
Tactic: rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
a : ℕ
⊢ log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
have negSucc : log (x ^ (a + 1))⁻¹ = (↑(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
a : ℕ
negSucc : log (x ^ (a + 1))⁻¹ = (↑(Int.negSucc a) : ℝ) * log x
⊢ log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
have negSucc₁ : -log (x ^ (a + 1)) = (↑(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
a : ℕ
negSucc : log (x ^ (a + 1))⁻¹ = (↑(Int.negSucc a) : ℝ) * log x
negSucc₁ : -log (x ^ (a + 1)) = (↑(Int.negSucc a) : ℝ) * log x
⊢ log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
have negSucc₂ : -((↑(a + 1) : ℝ) * log x) = (↑(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
have negSucc₃ : -((↑(a + 1) : ℝ) * log x) = -(↑(a + 1) : ℝ) * log x
Tactic: rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
have negSucc₄ : -(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x) = -HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x
Tactic: rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log (x ^ Int.negSucc a) = (↑(Int.negSucc a) : ℝ) * log x
have negSucc₅ : -HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x = -HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 * log x
Tactic: rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log √x = log x / 2
have rw : Ne (α := ℝ) 2 0
Tactic: rw [eq_div_iff, mul_comm, ← Nat.cast_two, ← log_pow, sq_sqrt hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1
have rw : log x + 1 ≤ x
Tactic: rw [le_sub_iff_add_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
have h : x = rexp (log x)
Tactic: convert! add_one_le_exp (log x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ x = rexp (log x)
have h : x = x
Tactic: rw [exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log x ≤ x
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ 0
Tactic: obtain rfl | hx := hx.eq_or_lt
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ 0
⊢ log x ≤ x
have inr : ∀ (hx : 0 < x), log x ≤ x
Tactic: obtain rfl | hx := hx.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ x - 1 ≤ x
have linarith : x < x - 1 → -1 + (x - (x - 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ -x⁻¹ ≤ log x
have rw : log x⁻¹ ≤ x⁻¹
Tactic: rw [neg_le, ← log_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ |log x * x| < 1
have this : 0 < 1 / x
Tactic: have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1