awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
x : ℝ
hx : x ≠ 0
this : Membership.mem (γ := Set ℝ) {0}ᶜ x
⊢ DifferentiableAt ℝ negMulLog x
have this₁ : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
Tactic: have := differentiableOn_negMulLog x this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : x ≠ 0
this_1 : Membership.mem (γ := Set ℝ) {0}ᶜ x
this mpr : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableAt ℝ negMulLog x
have mpr₁ : {0}ᶜ ∈ 𝓝 x
Tactic: apply DifferentiableWithinAt.differentiableAt (s := {0}ᶜ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ deriv negMulLog x = -log x - 1
have rw : -(log x + 1) = -log x - 1
Tactic: rw [negMulLog_eq_neg, deriv.fun_neg, deriv_mul_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt negMulLog (-log x - 1) x
have rw : DifferentiableAt ℝ negMulLog x
Tactic: rw [← deriv_negMulLog hx, hasDerivAt_deriv_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x
have refine : {0}ᶜ ∈ 𝓝 x
Tactic: refine DifferentiableOn.differentiableAt differentiableOn_negMulLog ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
⊢ deriv^[2] negMulLog x = -x⁻¹
have rw : deriv^[2] (fun (x : ℝ) ↦ -(x * log x)) x = -x⁻¹
Tactic: rw [negMulLog_eq_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
x : ℝ
⊢ deriv^[2] (fun (x : ℝ) ↦ -(x * log x)) x = -x⁻¹
have h : ∀ (x : ℝ), deriv^[2] (fun (x : ℝ) ↦ x * log x) x = x⁻¹
Tactic: have h := deriv2_mul_log
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h : ∀ (x : ℝ), deriv^[2] (fun (x : ℝ) ↦ x * log x) x = x⁻¹
⊢ deriv^[2] (fun (x : ℝ) ↦ -(x * log x)) x = -x⁻¹
have simp : -deriv (deriv fun (i : ℝ) ↦ i * log i) x = -x⁻¹
Tactic: simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, deriv.fun_neg',
    Function.comp_apply] at h ⊢
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h : ∀ (x : ℝ), deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
⊢ -deriv (deriv fun (i : ℝ) ↦ i * log i) x = -x⁻¹
have rw : -x⁻¹ = -x⁻¹
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ -x * log x < 1 - x
have linarith : 1 - x ≤ -x * log x → 1 - x - -x * log x + (x - 1 - x * log x) = 0
Tactic: linarith [self_sub_one_lt_mul_log h0 h1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
⊢ x.negMulLog ≤ 1 - x
have inl : ∀ (h0 : LE.le (α := ℝ) 0 1), negMulLog 1 ≤ HSub.hSub (α := ℝ) 1 1
Tactic: rcases eq_or_ne x 1 with rfl | h1
Cleared hypotheses: x, h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
inl : ∀ (h0 : LE.le (α := ℝ) 0 1), negMulLog 1 ≤ HSub.hSub (α := ℝ) 1 1
⊢ x.negMulLog ≤ 1 - x
have inr : ∀ (h1 : x ≠ 1), x.negMulLog ≤ 1 - x
Tactic: rcases eq_or_ne x 1 with rfl | h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
⊢ log⁺ x - log⁺ x⁻¹ = log x
have rw : max 0 (log x) - max 0 (-log x) = log x
Tactic: rw [posLog_def, posLog_def, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
⊢ max 0 (log x) - max 0 (-log x) = log x
have pos : ∀ (h : 0 ≤ log x), max 0 (log x) - max 0 (-log x) = log x
Tactic: by_cases! h : 0 ≤ log x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
pos : ∀ (h : 0 ≤ log x), max 0 (log x) - max 0 (-log x) = log x
⊢ max 0 (log x) - max 0 (-log x) = log x
have neg : ∀ (h : log x < 0), max 0 (log x) - max 0 (-log x) = log x
Tactic: by_cases! h : 0 ≤ log x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
⊢ 2⁻¹ * (log x + |log x|) = log⁺ x
have pos : ∀ (hr : 0 ≤ log x), 2⁻¹ * (log x + |log x|) = log⁺ x
Tactic: by_cases! hr : 0 ≤ log x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
pos : ∀ (hr : 0 ≤ log x), 2⁻¹ * (log x + |log x|) = log⁺ x
⊢ 2⁻¹ * (log x + |log x|) = log⁺ x
have neg : ∀ (hr : log x < 0), 2⁻¹ * (log x + |log x|) = log⁺ x
Tactic: by_cases! hr : 0 ≤ log x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hr : 0 ≤ log x
⊢ 2⁻¹ * (log x + |log x|) = log⁺ x
have pos : 2⁻¹ * (log x + log x) = log x
Tactic: simp [posLog, hr, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
⊢ log⁺ x = 0 ↔ |x| ≤ 1
have rw : log⁺ |x| = 0 ↔ log |x| ≤ 0
Tactic: rw [← posLog_abs, ← log_nonpos_iff (abs_nonneg x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : 1 ≤ |x|
⊢ log⁺ x = log x
have simp : 0 ≤ log x
Tactic: simp only [posLog, sup_eq_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : 1 ≤ |x|
⊢ 0 ≤ log x
have rw : 0 ≤ log |x|
Tactic: rw [← log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
n : ℕ
⊢ log⁺ (↑n : ℝ) = log (↑n : ℝ)
have pos : ∀ (hn : n = 0), log⁺ (↑n : ℝ) = log (↑n : ℝ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
n : ℕ
pos : ∀ (hn : n = 0), log⁺ (↑n : ℝ) = log (↑n : ℝ)
⊢ log⁺ (↑n : ℝ) = log (↑n : ℝ)
have neg : ∀ (hn : ¬n = 0), log⁺ (↑n : ℝ) = log (↑n : ℝ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
⊢ log⁺ x ≤ log⁺ y
have simp : log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
Tactic: simp only [posLog, le_sup_iff, sup_le_iff, le_refl, true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
have pos : ∀ (h : log x ≤ 0), log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
Tactic: by_cases! h : log x ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
pos : ∀ (h : log x ≤ 0), log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
have neg : ∀ (h : 0 < log x), log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
Tactic: by_cases! h : log x ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : log x ≤ 0
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
have pos : ¬log x ≤ 0 → 0 ≤ log y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : log x ≤ 0
pos : ¬log x ≤ 0 → 0 ≤ log y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
have pos₁ : ¬log x ≤ 0 → log x ≤ log y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
have neg : 0 ≤ log y ∧ log x ≤ log y
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
⊢ 0 ≤ log y ∧ log x ≤ log y
have this : log x ≤ log y
Tactic: have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 h)) hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
this : log x ≤ log y
⊢ 0 ≤ log y ∧ log x ≤ log y
have neg : 0 ≤ log y
Tactic: simp only [this, and_true, ge_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
this : log x ≤ log y
⊢ 0 ≤ log y
have linarith : log y < 0 → 0 - log x + (log x - log y) + (log y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
n : ℕ
x : ℝ
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
have pos : ∀ (hn : n = 0), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
n : ℕ
x : ℝ
pos : ∀ (hn : n = 0), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
have neg : ∀ (hn : ¬n = 0), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
have pos : ∀ (hx : |x| ≤ 1), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
Tactic: by_cases hx : |x| ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
pos : ∀ (hx : |x| ≤ 1), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
have neg : ∀ (hx : ¬|x| ≤ 1), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
Tactic: by_cases hx : |x| ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (hypothesis)
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
hx : ¬|x| ≤ 1
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
have hx₁ : 1 < |x|
Tactic: rw [not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (hypothesis)
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
hx : 1 < |x|
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
have this : 1 ≤ |x ^ n|
Tactic: have : 1 ≤ |x ^ n| := by simp_all [one_le_pow₀, hx.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x y : ℝ
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y
have pos : ∀ (ha : x = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
Tactic: by_cases ha : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x y : ℝ
pos : ∀ (ha : x = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y
have neg : ∀ (ha : ¬x = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
Tactic: by_cases ha : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x y : ℝ
ha : ¬x = 0
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y
have pos : ∀ (hb : y = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
Tactic: by_cases hb : y = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x y : ℝ
ha : ¬x = 0
pos : ∀ (hb : y = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y
have neg : ∀ (hb : ¬y = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
Tactic: by_cases hb : y = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ max 0 (log (x * y)) ≤ max 0 (log x) + max 0 (log y)
have neg : max (HAdd.hAdd (α := ℝ) 0 0) (log x + log y) ≤ max 0 (log x) + max 0 (log y)
Tactic: nth_rw 1 [← add_zero 0, log_mul ha hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
x : ℝ
n : ℕ
⊢ log⁺ ((↑n : ℝ) * x) ≤ log (↑n : ℝ) + log⁺ x
have rw : log⁺ ((↑n : ℝ) * x) ≤ log⁺ (↑n : ℝ) + log⁺ x
Tactic: rw [← log_of_nat_eq_posLog]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) = log⁺ (f a * ∏ t ∈ s, f t)
have rw : log⁺ (f a * ∏ x ∈ s, f x) = log⁺ (f a * ∏ t ∈ s, f t)
Tactic: rw [Finset.prod_insert ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) = ∑ t ∈ insert a s, log⁺ (f t)
have rw : log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) = log⁺ (f a) + ∑ x ∈ s, log⁺ (f x)
Tactic: rw [Finset.sum_insert ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)
have calc : log⁺ (∏ t ∈ insert a s, f t) = log⁺ (f a * ∏ t ∈ s, f t)
Tactic: calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
calc : log⁺ (∏ t ∈ insert a s, f t) = log⁺ (f a * ∏ t ∈ s, f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)
have calc₁ : log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) = ∑ t ∈ insert a s, log⁺ (f t)
Tactic: calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
have empty : log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)
Tactic: induction s using Finset.induction with
  | empty => simp [posLog]
  | insert a s ha hs =>
    calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
empty : log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)),
  log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)
Tactic: induction s using Finset.induction with
  | empty => simp [posLog]
  | insert a s ha hs =>
    calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
have empty : log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp [posLog]
  | insert a s ha hs =>
    calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
empty : log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)),
  log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp [posLog]
  | insert a s ha hs =>
    calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have pos : ∀ (hs : s = ∅), log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
Tactic: by_cases! hs : s = ∅
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
pos : ∀ (hs : s = ∅), log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have neg : ∀ (hs : s.Nonempty), log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
Tactic: by_cases! hs : s = ∅
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have neg : ∀ (t_max : α) (ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|),
  log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
Tactic: obtain ⟨t_max, ht_max⟩ := s.exists_max_image (fun t ↦ |f t|) hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|
have rw : log⁺ (∑ t ∈ s, f t) = log⁺ (∑ t ∈ s, f t)
Tactic: rw [Real.posLog_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)
have apply : LE.le (α := ℝ) |∑ t ∈ s, f t| (∑ t ∈ s, |f t|)
Tactic: apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)
have apply : LE.le (α := ℝ) (∑ t ∈ s, |f t|) (∑ t ∈ s, |f t_max|)
Tactic: apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log (↑s.card : ℝ) + log⁺ |f t_max| ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have bc : log⁺ |f t_max| ≤ ∑ t ∈ s, log⁺ (f t)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ |f t_max| ≤ ∑ t ∈ s, log⁺ (f t)
have bc : log⁺ (f t_max) ≤ ∑ t ∈ s, log⁺ (f t)
Tactic: rw [posLog_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have calc : log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|
Tactic: calc log⁺ (∑ t ∈ s, f t)
  _ = log⁺ |∑ t ∈ s, f t| := by
    rw [Real.posLog_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t|) := by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
  _ = log⁺ (s.card * |f t_max|) := by
    simp [Finset.sum_const]
  _ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
  _ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
    gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
calc : log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have calc₁ : log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)
Tactic: calc log⁺ (∑ t ∈ s, f t)
  _ = log⁺ |∑ t ∈ s, f t| := by
    rw [Real.posLog_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t|) := by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
  _ = log⁺ (s.card * |f t_max|) := by
    simp [Finset.sum_const]
  _ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
  _ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
    gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
calc : log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|
calc₁ : log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have calc₂ : log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)
Tactic: calc log⁺ (∑ t ∈ s, f t)
  _ = log⁺ |∑ t ∈ s, f t| := by
    rw [Real.posLog_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t|) := by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
  _ = log⁺ (s.card * |f t_max|) := by
    simp [Finset.sum_const]
  _ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
  _ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
    gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.PosLog (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
calc : log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|
calc₁ : log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)
calc₂ : log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
have calc₃ : log⁺ (∑ t ∈ s, |f t_max|) = log⁺ ((↑s.card : ℝ) * |f t_max|)
Tactic: calc log⁺ (∑ t ∈ s, f t)
  _ = log⁺ |∑ t ∈ s, f t| := by
    rw [Real.posLog_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t|) := by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
  _ = log⁺ (s.card * |f t_max|) := by
    simp [Finset.sum_const]
  _ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
  _ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
    gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1