awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x ∈ Ico x₀ (r ^ (⌊logb r (x / x₀)⌋₊ + 1) * x₀)
have rw : x₀ ≤ x ∧ logb r (x / x₀) < HAdd.hAdd (α := ℝ) (↑⌊logb r (x / x₀)⌋₊ : ℝ) 1
Tactic: rw [mem_Ico, ← div_lt_iff₀ hx₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add,
      Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
⊢ ∀ x ≥ x₀, P x
have suffices : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
Tactic: suffices ∀ n : ℕ, ∀ x ∈ Set.Ico x₀ (r ^ (n + 1) * x₀), P x by
    intro x hx
    have hx' : 0 < x / x₀ := div_pos (hx₀.trans_le hx) hx₀
    refine this ⌊logb r (x / x₀)⌋₊ x ?_
    rw [mem_Ico, ← div_lt_iff₀ hx₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add,
      Nat.cast_one]
    exact ⟨hx, Nat.lt_floor_add_one _⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
⊢ ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
have zero : ∀ x ∈ Ico x₀ (r ^ HAdd.hAdd (α := ℕ) 0 1 * x₀), P x
Tactic: induction n with
  | zero => simpa using base
  | succ n ih =>
    exact fun x hx => (Ico_subset_Ico_union_Ico hx).elim (ih x) (step (n + 1) (by simp) ih _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
zero : ∀ x ∈ Ico x₀ (r ^ HAdd.hAdd (α := ℕ) 0 1 * x₀), P x
⊢ ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
have succ : ∀ (n : ℕ) (ih : ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x), ∀ x ∈ Ico x₀ (r ^ (n + 1 + 1) * x₀), P x
Tactic: induction n with
  | zero => simpa using base
  | succ n ih =>
    exact fun x hx => (Ico_subset_Ico_union_Ico hx).elim (ih x) (step (n + 1) (by simp) ih _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ log x =
    (expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx)
have rw : Eq (α := ℝ)
  ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| sorry) :
    ℝ)
  ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx) :
    ℝ)
Tactic: rw [log_of_ne_zero hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ Eq (α := ℝ)
    ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯) :
      ℝ)
    ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx) :
      ℝ)
have h : |x| = x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ rexp (log x) = |x|
have rw : rexp
    ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| sorry)) =
  |x|
Tactic: rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x ≠ 0
rw :
  rexp
      ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯)) =
    |x|
⊢ rexp (log x) = |x|
have rw₁ : (↑((expOrderIso : (a : ℝ) → (↑(Ioi 0) : Type))
        ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
          (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| sorry))) :
    ℝ) =
  |x|
Tactic: rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x ≠ 0
rw :
  rexp
      ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯)) =
    |x|
rw₁ :
  (↑((expOrderIso : (a : ℝ) → (↑(Ioi 0) : Type))
          ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
            (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯))) :
      ℝ) =
    |x|
⊢ rexp (log x) = |x|
have rw₂ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| sorry) : ℝ) = |x|
Tactic: rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x ≠ 0
rw :
  rexp
      ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯)) =
    |x|
rw₁ :
  (↑((expOrderIso : (a : ℝ) → (↑(Ioi 0) : Type))
          ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
            (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯))) :
      ℝ) =
    |x|
rw₂ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯) : ℝ) = |x|
⊢ rexp (log x) = |x|
have rw₃ : |x| = |x|
Tactic: rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ rexp (log x) = x
have rw : |x| = x
Tactic: rw [exp_log_eq_abs hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : x < 0
⊢ rexp (log x) = -x
have rw : |x| = -x
Tactic: rw [exp_log_eq_abs (ne_of_lt hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ x ≤ rexp (log x)
have pos : ∀ (h_zero : x = 0), x ≤ rexp (log x)
Tactic: by_cases h_zero : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
pos : ∀ (h_zero : x = 0), x ≤ rexp (log x)
⊢ x ≤ rexp (log x)
have neg : ∀ (h_zero : ¬x = 0), x ≤ rexp (log x)
Tactic: by_cases h_zero : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h_zero : x = 0
⊢ x ≤ rexp (log x)
have pos : LE.le (α := ℝ) 0 1
Tactic: rw [h_zero, log, dif_pos rfl, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)
have neg : x ≤ |x|
Tactic: rw [exp_log_eq_abs h_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ rexp 1 * x ≤ rexp x
have pos : ∀ (hx0 : x ≤ 0), rexp 1 * x ≤ rexp x
Tactic: by_cases hx0 : x ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
pos : ∀ (hx0 : x ≤ 0), rexp 1 * x ≤ rexp x
⊢ rexp 1 * x ≤ rexp x
have neg : ∀ (hx0 : ¬x ≤ 0), rexp 1 * x ≤ rexp x
Tactic: by_cases hx0 : x ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x
have h : log x + 1 ≤ rexp (log x)
Tactic: have h := add_one_le_exp (log x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx0 : ¬x ≤ 0
h : log x + 1 ≤ rexp (log x)
⊢ rexp 1 * x ≤ rexp x
have neg : ∀ (h : rexp (log x + 1) ≤ rexp (rexp (log x))), rexp 1 * x ≤ rexp x
Tactic: rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_ge hx0), mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ rexp 1 * x ≤ rexp x
have neg₁ : ∀ (h : rexp (log x) * rexp 1 ≤ rexp (rexp (log x))), rexp 1 * x ≤ rexp x
Tactic: rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_ge hx0), mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ rexp 1 * x ≤ rexp x
have neg₂ : ∀ (h : x * rexp 1 ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ rexp 1 * x ≤ rexp x
have neg₃ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ 2 * x ≤ rexp x
have pos : ∀ (hx0 : x < 0), 2 * x ≤ rexp x
Tactic: by_cases hx0 : x < 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
pos : ∀ (hx0 : x < 0), 2 * x ≤ rexp x
⊢ 2 * x ≤ rexp x
have neg : ∀ (hx0 : ¬x < 0), 2 * x ≤ rexp x
Tactic: by_cases hx0 : x < 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x
have apply : 2 ≤ rexp 1
Tactic: apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
hx0 : ¬x < 0
⊢ 2 ≤ rexp 1
have this : HAdd.hAdd (α := ℝ) 1 1 ≤ rexp 1
Tactic: have := Real.add_one_le_exp 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx0 : ¬x < 0
this : HAdd.hAdd (α := ℝ) 1 1 ≤ rexp 1
⊢ 2 ≤ rexp 1
have rwa : ∀ (this : 2 ≤ rexp 1), 2 ≤ rexp 1
Tactic: rwa [one_add_one_eq_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
⊢ rexp (log 1) = rexp 0
have rw : 1 = rexp 0
Tactic: rw [exp_log zero_lt_one, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
rw : 1 = rexp 0
⊢ rexp (log 1) = rexp 0
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [exp_log zero_lt_one, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ log (x / x) = 0
have inl : log (0 / 0) = 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
inl : log (0 / 0) = 0
⊢ log (x / x) = 0
have inr : ∀ (hx : x ≠ 0), log (x / x) = 0
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ log |x| = log x
have pos : ∀ (h : x = 0), log |x| = log x
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
pos : ∀ (h : x = 0), log |x| = log x
⊢ log |x| = log x
have neg : ∀ (h : ¬x = 0), log |x| = log x
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : ¬x = 0
⊢ log |x| = log x
have neg : rexp (log |x|) = rexp (log x)
Tactic: rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : ¬x = 0
neg : rexp (log |x|) = rexp (log x)
⊢ log |x| = log x
have neg₁ : rexp (log |x|) = |x|
Tactic: rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : ¬x = 0
neg : rexp (log |x|) = rexp (log x)
neg₁ : rexp (log |x|) = |x|
⊢ log |x| = log x
have neg₂ : |(|x|)| = |x|
Tactic: rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : ¬x = 0
neg : rexp (log |x|) = rexp (log x)
neg₁ : rexp (log |x|) = |x|
neg₂ : |(|x|)| = |x|
⊢ log |x| = log x
have neg₃ : |x| = |x|
Tactic: rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ log (-x) = log x
have rw : log (-x) = log |x|
Tactic: rw [← log_abs x, ← log_abs (-x), abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
rw : log (-x) = log |x|
⊢ log (-x) = log x
have rw₁ : log |(-x)| = log |x|
Tactic: rw [← log_abs x, ← log_abs (-x), abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
rw : log (-x) = log |x|
rw₁ : log |(-x)| = log |x|
⊢ log (-x) = log x
have rw₂ : log |x| = log |x|
Tactic: rw [← log_abs x, ← log_abs (-x), abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ sinh (log x) = (x - x⁻¹) / 2
have rw : (rexp (log x) - rexp (-log x)) / 2 = (x - x⁻¹) / 2
Tactic: rw [sinh_eq, exp_neg, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
rw : (rexp (log x) - rexp (-log x)) / 2 = (x - x⁻¹) / 2
⊢ sinh (log x) = (x - x⁻¹) / 2
have rw₁ : (rexp (log x) - (rexp (log x))⁻¹) / 2 = (x - x⁻¹) / 2
Tactic: rw [sinh_eq, exp_neg, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ sinh (log x) = (x - x⁻¹) / 2
have rw₂ : (x - x⁻¹) / 2 = (x - x⁻¹) / 2
Tactic: rw [sinh_eq, exp_neg, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ cosh (log x) = (x + x⁻¹) / 2
have rw : (rexp (log x) + rexp (-log x)) / 2 = (x + x⁻¹) / 2
Tactic: rw [cosh_eq, exp_neg, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : 0 < x
rw : (rexp (log x) + rexp (-log x)) / 2 = (x + x⁻¹) / 2
⊢ cosh (log x) = (x + x⁻¹) / 2
have rw₁ : (rexp (log x) + (rexp (log x))⁻¹) / 2 = (x + x⁻¹) / 2
Tactic: rw [cosh_eq, exp_neg, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ cosh (log x) = (x + x⁻¹) / 2
have rw₂ : (x + x⁻¹) / 2 = (x + x⁻¹) / 2
Tactic: rw [cosh_eq, exp_neg, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
⊢ log (-rexp x) = x
have rw : log (rexp x) = x
Tactic: rw [log_neg_eq_log, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) univ x
rw : log (rexp x) = x
⊢ log (-rexp x) = x
have rw₁ : x = x
Tactic: rw [log_neg_eq_log, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x * y)) = rexp (log x + log y)
have rw : |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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
rw : |x * y| = rexp (log x + log y)
⊢ rexp (log (x * y)) = rexp (log x + log y)
have rw₁ : |x * y| = rexp (log x) * rexp (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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)
⊢ rexp (log (x * y)) = rexp (log x + log y)
have rw₂ : |x * y| = |x| * rexp (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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)
⊢ rexp (log (x * y)) = rexp (log x + log y)
have rw₃ : |x * y| = |x| * |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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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|
⊢ rexp (log (x * y)) = rexp (log x + log y)
have rw₄ : |x| * |y| = |x| * |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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x / y)) = rexp (log x - log y)
have rw : |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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
rw : |x / y| = rexp (log x - log y)
⊢ rexp (log (x / y)) = rexp (log x - log y)
have rw₁ : |x / y| = rexp (log x) / rexp (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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)
⊢ rexp (log (x / y)) = rexp (log x - log y)
have rw₂ : |x / y| = |x| / rexp (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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)
⊢ rexp (log (x / y)) = rexp (log x - log y)
have rw₃ : |x / y| = |x| / |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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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|
⊢ rexp (log (x / y)) = rexp (log x - log y)
have rw₄ : |x| / |y| = |x| / |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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ log x⁻¹ = -log x
have pos : ∀ (hx : x = 0), log x⁻¹ = -log x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
pos : ∀ (hx : x = 0), log x⁻¹ = -log x
⊢ log x⁻¹ = -log x
have neg : ∀ (hx : ¬x = 0), log x⁻¹ = -log x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x
have neg : rexp (log x⁻¹) = rexp (-log x)
Tactic: rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : ¬x = 0
neg : rexp (log x⁻¹) = rexp (-log x)
⊢ log x⁻¹ = -log x
have neg₁ : |x⁻¹| = rexp (-log x)
Tactic: rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : ¬x = 0
neg : rexp (log x⁻¹) = rexp (-log x)
neg₁ : |x⁻¹| = rexp (-log x)
⊢ log x⁻¹ = -log x
have neg₂ : |x⁻¹| = (rexp (log x))⁻¹
Tactic: rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
hx : ¬x = 0
neg : rexp (log x⁻¹) = rexp (-log x)
neg₁ : |x⁻¹| = rexp (-log x)
neg₂ : |x⁻¹| = (rexp (log x))⁻¹
⊢ log x⁻¹ = -log x
have neg₃ : |x⁻¹| = |x|⁻¹
Tactic: rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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|⁻¹
⊢ log x⁻¹ = -log x
have neg₄ : |x|⁻¹ = |x|⁻¹
Tactic: rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ log x ≤ log y ↔ x ≤ y
have rw : rexp (log x) ≤ rexp (log y) ↔ x ≤ y
Tactic: rw [← exp_le_exp, exp_log h, exp_log h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
h : 0 < x
h₁ : 0 < y
rw : rexp (log x) ≤ rexp (log y) ↔ x ≤ y
⊢ log x ≤ log y ↔ x ≤ y
have rw₁ : x ≤ rexp (log y) ↔ x ≤ y
Tactic: rw [← exp_le_exp, exp_log h, exp_log h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log x ≤ log y ↔ x ≤ y
have rw₂ : x ≤ y ↔ x ≤ y
Tactic: rw [← exp_le_exp, exp_log h, exp_log h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
h : x < y
⊢ log x < log y
have rwa : rexp (log x) < rexp (log y)
Tactic: rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
h : x < y
rwa : rexp (log x) < rexp (log y)
⊢ log x < log y
have rwa₁ : x < rexp (log y)
Tactic: rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y
have rw : rexp (log x) < rexp (log y) ↔ x < y
Tactic: rw [← exp_lt_exp, exp_log hx, exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
hy : 0 < y
rw : rexp (log x) < rexp (log y) ↔ x < y
⊢ log x < log y ↔ x < y
have rw₁ : x < rexp (log y) ↔ x < y
Tactic: rw [← exp_lt_exp, exp_log hx, exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ log x < log y ↔ x < y
have rw₂ : x < y ↔ x < y
Tactic: rw [← exp_lt_exp, exp_log hx, exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
⊢ log x ≤ y ↔ x ≤ rexp y
have rw : rexp (log x) ≤ rexp y ↔ x ≤ rexp y
Tactic: rw [← exp_le_exp, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x) ≤ rexp y ↔ x ≤ rexp y
⊢ log x ≤ y ↔ x ≤ rexp y
have rw₁ : x ≤ rexp y ↔ x ≤ rexp y
Tactic: rw [← exp_le_exp, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
⊢ log x < y ↔ x < rexp y
have rw : rexp (log x) < rexp y ↔ x < rexp y
Tactic: rw [← exp_lt_exp, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x) < rexp y ↔ x < rexp y
⊢ log x < y ↔ x < rexp y
have rw₁ : x < rexp y ↔ x < rexp y
Tactic: rw [← exp_lt_exp, exp_log hx]