awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
rw : HasSum term (log (1 + x) - log (1 - x))
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
have rw₁ : ∀ x ∉ Set.range fun (x : ℕ) ↦ 2 * x, term x = 0
Tactic: rw [← h_term_eq_goal, (mul_right_injective₀ (two_ne_zero' ℕ)).hasSum_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))
have h₁ : HasSum (fun (i : ℕ) ↦ -1 * ((-x) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) (-1 * -log (1 - -x))
Tactic: have h₁ := (hasSum_pow_div_log_of_abs_lt_one (Eq.trans_lt (abs_neg x) h)).mul_left (-1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun (i : ℕ) ↦ -1 * ((-x) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) (-1 * -log (1 - -x))
⊢ HasSum term (log (1 + x) - log (1 - x))
have h₂ : log (1 + x) - log (1 - x) = -1 * -log (1 - -x) + -log (1 - x)
Tactic: convert! h₁.add (hasSum_pow_div_log_of_abs_lt_one h) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : m ∉ Set.range fun (x : ℕ) ↦ 2 * x
⊢ term m = 0
have hm₁ : Even (m + 1)
Tactic: rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ -1 * ((-x) ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
have rw : -1 * (x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
Tactic: rw [Even.neg_pow hm, neg_one_mul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
rw : -1 * (x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
⊢ -1 * ((-x) ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
have rw₁ : -(x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
Tactic: rw [Even.neg_pow hm, neg_one_mul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
rw : -1 * (x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
rw₁ : -(x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
⊢ -1 * ((-x) ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [Even.neg_pow hm, neg_one_mul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
⊢ |1 / (2 * a + 1)| < 1
have rw : 1 < 2 * a + 1
Tactic: rw [abs_of_pos, div_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
rw : 1 < 2 * a + 1
⊢ |1 / (2 * a + 1)| < 1
have rw₁ : 0 < 2 * a + 1
Tactic: rw [abs_of_pos, div_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
rw : 1 < 2 * a + 1
rw₁ : 0 < 2 * a + 1
⊢ |1 / (2 * a + 1)| < 1
have rw₂ : 0 < 1 / (2 * a + 1)
Tactic: rw [abs_of_pos, div_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1
have linarith : 2 * a + 1 ≤ 1 → 2 * (0 - a) + (2 * a + 1 - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
linarith : 2 * a + 1 ≤ 1 → 2 * (0 - a) + (2 * a + 1 - 1) = 0
⊢ 1 < 2 * a + 1
have linarith₁ : 2 * a + 1 ≤ 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1
have linarith : 2 * a + 1 ≤ 0 → -1 + 2 * (0 - a) + (2 * a + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
linarith : 2 * a + 1 ≤ 0 → -1 + 2 * (0 - a) + (2 * a + 1 - 0) = 0
⊢ 0 < 2 * a + 1
have linarith₁ : 2 * a + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
a : ℝ
h : 0 < a
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
have h₁ : |1 / (2 * a + 1)| < 1
Tactic: have h₁ : |1 / (2 * a + 1)| < 1 := by
    rw [abs_of_pos, div_lt_one]
    · linarith
    · linarith
    · exact div_pos one_pos (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
have h₂ : log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
Tactic: convert! hasSum_log_sub_log_of_abs_lt_one h₁ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ 2 * a + 1 ≠ 0
have linarith : 2 * a + 1 = 0 → -1 + 2 * (0 - a) + (2 * a + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
linarith : 2 * a + 1 = 0 → -1 + 2 * (0 - a) + (2 * a + 1 - 0) = 0
⊢ 2 * a + 1 ≠ 0
have linarith₁ : 2 * a + 1 = 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
have h₂ : 2 * a + 1 ≠ 0
Tactic: have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
have h₃ : a ≠ 0
Tactic: have h₃ := h.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
have h₄ : log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
Tactic: rw [← log_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
h₄ : log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
have h₅ : 1 + 1 / (2 * a + 1) ≠ 0
Tactic: rw [← log_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
h₄ : log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
h₅ : 1 + 1 / (2 * a + 1) ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
have h₆ : 1 - 1 / (2 * a + 1) ≠ 0
Tactic: rw [← log_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
have h₄ : 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))
have h₄ : (a + 1) * 2 = a * 2 + 1 + 1
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0
have h₄ : (2 * a + 1 + 1) / (2 * a + 1) ≠ 0
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 ≤ a
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))
have inl : ∀ (h : LE.le (α := ℝ) 0 0),
  HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (0 / HAdd.hAdd (α := ℝ) 0 2) ^ (2 * k + 1))
    (log (HAdd.hAdd (α := ℝ) 1 0))
Tactic: obtain (rfl | ha0) := eq_or_ne a 0
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 ≤ a
inl :
  ∀ (h : LE.le (α := ℝ) 0 0),
    HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (0 / HAdd.hAdd (α := ℝ) 0 2) ^ (2 * k + 1))
      (log (HAdd.hAdd (α := ℝ) 1 0))
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))
have inr : ∀ (ha0 : a ≠ 0),
  HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))
Tactic: obtain (rfl | ha0) := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))
have h₁ : ∀ (x : ℕ), a / (a + 2) = 1 / (2 * a⁻¹ + 1)
Tactic: convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
h₁ : ∀ (x : ℕ), a / (a + 2) = 1 / (2 * a⁻¹ + 1)
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))
have h₂ : a = a⁻¹⁻¹
Tactic: convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) ≤ log (1 + x)
have h : 2 * x / (x + 2) = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1)) * (x / (x + 2)) ^ (HMul.hMul (α := ℕ) 2 0 + 1)
Tactic: convert! le_hasSum (hasSum_log_one_add hx) 0 (by intros; positivity) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) < log (1 + x)
have h : 2 * x / (x + 2) = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1)) * (x / (x + 2)) ^ (HMul.hMul (α := ℕ) 2 0 + 1)
Tactic: convert!
    lt_hasSum (hasSum_log_one_add hx.le) 0 (by intros; positivity) 1 (by positivity)
      (by positivity) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ
⊢ (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)
have simp : (if x ≤ 0 then ⊥ else (↑(Real.log (ENNReal.ofReal x).toReal) : EReal)) = if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)
Tactic: simp only [log, ENNReal.ofReal_ne_top,
    ENNReal.ofReal_eq_zero, if_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ
⊢ (if x ≤ 0 then ⊥ else (↑(Real.log (ENNReal.ofReal x).toReal) : EReal)) = if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)
have pos : ∀ (h_nonpos : x ≤ 0), Eq (α := EReal) ⊥ ⊥
Tactic: split_ifs with h_nonpos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ
pos : ∀ (h_nonpos : x ≤ 0), Eq (α := EReal) ⊥ ⊥
⊢ (if x ≤ 0 then ⊥ else (↑(Real.log (ENNReal.ofReal x).toReal) : EReal)) = if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)
have neg : ∀ (h_nonpos : ¬x ≤ 0), (↑(Real.log (ENNReal.ofReal x).toReal) : EReal) = (↑(Real.log x) : EReal)
Tactic: split_ifs with h_nonpos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ
h_nonpos : ¬x ≤ 0
⊢ (↑(Real.log (ENNReal.ofReal x).toReal) : EReal) = (↑(Real.log x) : EReal)
have neg : (↑(Real.log x) : EReal) = (↑(Real.log x) : EReal)
Tactic: rw [ENNReal.toReal_ofReal (not_le.mp h_nonpos).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ (ENNReal.ofReal x).log = (↑(Real.log x) : EReal)
have rw : (if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)) = (↑(Real.log x) : EReal)
Tactic: rw [log_ofReal, if_neg hx.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ
hx : 0 < x
rw : (if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)) = (↑(Real.log x) : EReal)
⊢ (ENNReal.ofReal x).log = (↑(Real.log x) : EReal)
have rw₁ : (↑(Real.log x) : EReal) = (↑(Real.log x) : EReal)
Tactic: rw [log_ofReal, if_neg hx.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have pos₂ : ¬x = 0 → x = ∞ → y = 0 → LT.lt (α := EReal) ⊤ ⊥
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
pos₂ : ¬x = 0 → x = ∞ → y = 0 → LT.lt (α := EReal) ⊤ ⊥
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have pos₃ : ¬x = 0 → x = ∞ → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊤ ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
pos₂ : ¬x = 0 → x = ∞ → y = 0 → LT.lt (α := EReal) ⊤ ⊥
pos₃ : ¬x = 0 → x = ∞ → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊤ ⊤
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have neg₁ : ¬x = 0 → x = ∞ → ¬y = 0 → ¬y = ∞ → ⊤ < (↑(Real.log y.toReal) : EReal)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
pos₂ : ¬x = 0 → x = ∞ → y = 0 → LT.lt (α := EReal) ⊤ ⊥
pos₃ : ¬x = 0 → x = ∞ → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊤ ⊤
neg₁ : ¬x = 0 → x = ∞ → ¬y = 0 → ¬y = ∞ → ⊤ < (↑(Real.log y.toReal) : EReal)
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have pos₄ : ¬x = 0 → ¬x = ∞ → y = 0 → (↑(Real.log x.toReal) : EReal) < ⊥
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
pos₂ : ¬x = 0 → x = ∞ → y = 0 → LT.lt (α := EReal) ⊤ ⊥
pos₃ : ¬x = 0 → x = ∞ → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊤ ⊤
neg₁ : ¬x = 0 → x = ∞ → ¬y = 0 → ¬y = ∞ → ⊤ < (↑(Real.log y.toReal) : EReal)
pos₄ : ¬x = 0 → ¬x = ∞ → y = 0 → (↑(Real.log x.toReal) : EReal) < ⊥
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have pos₅ : ¬x = 0 → ¬x = ∞ → ¬y = 0 → y = ∞ → (↑(Real.log x.toReal) : EReal) < ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
pos₂ : ¬x = 0 → x = ∞ → y = 0 → LT.lt (α := EReal) ⊤ ⊥
pos₃ : ¬x = 0 → x = ∞ → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊤ ⊤
neg₁ : ¬x = 0 → x = ∞ → ¬y = 0 → ¬y = ∞ → ⊤ < (↑(Real.log y.toReal) : EReal)
pos₄ : ¬x = 0 → ¬x = ∞ → y = 0 → (↑(Real.log x.toReal) : EReal) < ⊥
pos₅ : ¬x = 0 → ¬x = ∞ → ¬y = 0 → y = ∞ → (↑(Real.log x.toReal) : EReal) < ⊤
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)
have neg₂ : ¬x = 0 → ¬x = ∞ → ¬y = 0 → ¬y = ∞ → (↑(Real.log x.toReal) : EReal) < (↑(Real.log y.toReal) : EReal)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
⊢ ∃ (a : ℝ≥0∞), a.log = ⊥
have h : log 0 = ⊥
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
⊢ ∃ (a : ℝ≥0∞), a.log = ⊤
have h : log ∞ = ⊤
Tactic: use ⊤
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ
⊢ ∃ (a : ℝ≥0∞), a.log = (↑y : EReal)
have h : (ENNReal.ofReal (Real.exp y)).log = (↑y : EReal)
Tactic: use ENNReal.ofReal (Real.exp y)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : EReal
⊢ ∃ (a : ℝ≥0∞), a.log = y
have bot : ∃ (a : ℝ≥0∞), a.log = ⊥
Tactic: cases y with
  | bot => use 0; simp
  | top => use ⊤; simp
  | coe y => use ENNReal.ofReal (Real.exp y); simp [Real.exp_pos]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : EReal
bot : ∃ (a : ℝ≥0∞), a.log = ⊥
⊢ ∃ (a : ℝ≥0∞), a.log = y
have top : ∃ (a : ℝ≥0∞), a.log = ⊤
Tactic: cases y with
  | bot => use 0; simp
  | top => use ⊤; simp
  | coe y => use ENNReal.ofReal (Real.exp y); simp [Real.exp_pos]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : EReal
bot : ∃ (a : ℝ≥0∞), a.log = ⊥
top : ∃ (a : ℝ≥0∞), a.log = ⊤
⊢ ∃ (a : ℝ≥0∞), a.log = y
have coe : ∀ (y : ℝ), ∃ (a : ℝ≥0∞), a.log = (↑y : EReal)
Tactic: cases y with
  | bot => use 0; simp
  | top => use ⊤; simp
  | coe y => use ENNReal.ofReal (Real.exp y); simp [Real.exp_pos]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
⊢ (x * y).log = x.log + y.log
have inl : (0 * y).log = log 0 + y.log
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
inl : (0 * y).log = log 0 + y.log
⊢ (x * y).log = x.log + y.log
have inr : (∞ * y).log = log ∞ + y.log
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
inl : (0 * y).log = log 0 + y.log
inr : (∞ * y).log = log ∞ + y.log
⊢ (x * y).log = x.log + y.log
have inr₁ : ∀ (x_real : 0 < x.toReal), (x * y).log = x.log + y.log
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ≥0∞
⊢ (∞ * y).log = ⊤ + y.log
have inr : (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0
Tactic: rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ≥0∞
inr : (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0
⊢ (∞ * y).log = ⊤ + y.log
have inr₁ : (HMul.hMul (α := ℝ≥0∞) ∞ ∞).log = ⊤ + log ∞
Tactic: rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ≥0∞
inr : (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0
inr₁ : (HMul.hMul (α := ℝ≥0∞) ∞ ∞).log = ⊤ + log ∞
⊢ (∞ * y).log = ⊤ + y.log
have inr₂ : ∀ (y_real : 0 < y.toReal), (∞ * y).log = ⊤ + y.log
Tactic: rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
⊢ (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0
have inr : log 0 = ⊤ + log 0
Tactic: rw [mul_zero, log_zero, EReal.add_bot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
inr : log 0 = ⊤ + log 0
⊢ (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0
have inr₁ : ⊥ = HAdd.hAdd (α := EReal) ⊤ ⊥
Tactic: rw [mul_zero, log_zero, EReal.add_bot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
inr : log 0 = ⊤ + log 0
inr₁ : ⊥ = HAdd.hAdd (α := EReal) ⊤ ⊥
⊢ (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0
have inr₂ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [mul_zero, log_zero, EReal.add_bot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log
have inr : Eq (α := ℝ≥0∞) (if y = 0 then 0 else ∞) ∞
Tactic: rw [log_pos_real' y_real, ENNReal.top_mul', EReal.top_add_coe, log_eq_top_iff]