awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ |log x * x| < 1
have this₁ : log (1 / x) ≤ 1 / x - 1
Tactic: replace := log_le_sub_one_of_pos this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ log (1 / x) < 1 / x
have linarith : 1 / x ≤ log (1 / x) →
  -1 + (1 * log (1 / x) - (1 * (1 / x) - HMul.hMul (α := ℝ) 1 1)) + (1 * (1 / x) - 1 * log (1 / x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ |log x * x| < 1
have this₁ : log (1 / x) < 1 / x
Tactic: replace : log (1 / x) < 1 / x := by linarith
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ |log x * x| < 1
have this₁ : -log x * x < 1
Tactic: rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff₀ h1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x * x
have refine : 0 ≤ -log x
Tactic: refine mul_nonneg ?_ h1.le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x
have rw : 0 ≤ log x⁻¹
Tactic: rw [← log_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹
have hx : 1 ≤ x⁻¹
Tactic: apply log_nonneg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1
have aux : 0 ≤ -log x * x
Tactic: have aux : 0 ≤ -log x * x := by
    refine mul_nonneg ?_ h1.le
    rw [← log_inv]
    apply log_nonneg
    rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]
    exact h2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
⊢ ContinuousOn log {0}ᶜ
have simp : Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦ log (↑x : ℝ)
Tactic: simp +unfoldPartialApp only [continuousOn_iff_continuous_restrict,
    restrict]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : (↑{0}ᶜ : Type)
| log (↑x : ℝ)
have rw : ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
    (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |(↑x : ℝ)| sorry) :
  ℝ)
Tactic: rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦ log (↑x : ℝ)
have conv : Continuous (Y := ℝ) fun (x : (↑{0}ᶜ : Type)) ↦
  (expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
    (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |(↑x : ℝ)| sorry)
Tactic: conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
x : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0
have refine : ContinuousAt log x → x ≠ 0
Tactic: refine ⟨?_, continuousAt_log⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
a : ℝ
l : List ℝ
ih : ∀ (h : ∀ x ∈ l, x ≠ 0), log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ∀ x ∈ a :: l, x ≠ 0
⊢ log (a :: l).prod = sum (List.map (fun (x : ℝ) ↦ log x) (a :: l))
have ih₁ : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
Tactic: simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]
Cleared hypotheses: ih, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
a : ℝ
l : List ℝ
ih : ∀ (h : ∀ x ∈ l, x ≠ 0), log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ∀ x ∈ a :: l, x ≠ 0
ih₁ : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
⊢ log (a :: l).prod = sum (List.map (fun (x : ℝ) ↦ log x) (a :: l))
have h₁ : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
Tactic: simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]
Cleared hypotheses: ih, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
a : ℝ
l : List ℝ
ih : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
⊢ log (a * l.prod) = log a + sum (List.map (fun (x : ℝ) ↦ log x) l)
have this : l.prod ≠ 0
Tactic: have : l.prod ≠ 0 := by grind [prod_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
a : ℝ
l : List ℝ
ih : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
⊢ log (a * l.prod) = log a + sum (List.map (fun (x : ℝ) ↦ log x) l)
have cons : log a + log l.prod = log a + sum (List.map (fun (x : ℝ) ↦ log x) l)
Tactic: rw [log_mul h.1 this, add_right_inj, ih]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
a : ℝ
l : List ℝ
ih : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
cons : log a + log l.prod = log a + sum (List.map (fun (x : ℝ) ↦ log x) l)
cons₁ : log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
⊢ log (a * l.prod) = log a + sum (List.map (fun (x : ℝ) ↦ log x) l)
have cons₂ : Eq (α := ℝ) (sum (List.map (fun (x : ℝ) ↦ log x) l)) (sum (List.map (fun (x : ℝ) ↦ log x) l))
Tactic: rw [log_mul h.1 this, add_right_inj, ih]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
l : List ℝ
h : ∀ x ∈ l, x ≠ 0
⊢ log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
have nil : ∀ (h : ∀ (x : ℝ), Membership.mem (γ := List ℝ) [] x → x ≠ 0),
  log (List.prod []) = sum (List.map (fun (x : ℝ) ↦ log x) [])
Tactic: induction l with
  | nil => simp
  | cons a l ih =>
    simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]
    have : l.prod ≠ 0 := by grind [prod_ne_zero]
    rw [log_mul h.1 this, add_right_inj, ih]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
l : List ℝ
h : ∀ x ∈ l, x ≠ 0
nil :
  ∀ (h : ∀ (x : ℝ), Membership.mem (γ := List ℝ) [] x → x ≠ 0),
    log (List.prod []) = sum (List.map (fun (x : ℝ) ↦ log x) [])
⊢ log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l)
have cons : ∀ (a : ℝ) (l : List ℝ) (ih : ∀ (h : ∀ x ∈ l, x ≠ 0), log l.prod = sum (List.map (fun (x : ℝ) ↦ log x) l))
  (h : ∀ x ∈ a :: l, x ≠ 0), log (a :: l).prod = sum (List.map (fun (x : ℝ) ↦ log x) (a :: l))
Tactic: induction l with
  | nil => simp
  | cons a l ih =>
    simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]
    have : l.prod ≠ 0 := by grind [prod_ne_zero]
    rw [log_mul h.1 this, add_right_inj, ih]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ log s.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)
have rw : log s.toList.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)
Tactic: rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
rw : log s.toList.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)
⊢ log s.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)
have rw₁ : Eq (α := ℝ) (List.sum (List.map (fun (x : ℝ) ↦ log x) s.toList)) (sum (Multiset.map (fun (x : ℝ) ↦ log x) s))
Tactic: rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
rw : log s.toList.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)
rw₁ : Eq (α := ℝ) (List.sum (List.map (fun (x : ℝ) ↦ log x) s.toList)) (sum (Multiset.map (fun (x : ℝ) ↦ log x) s))
⊢ log s.prod = sum (Multiset.map (fun (x : ℝ) ↦ log x) s)
have rw₂ : Eq (α := ℝ) (sum (Multiset.map (fun (x : ℝ) ↦ log x) s)) (sum (Multiset.map (fun (x : ℝ) ↦ log x) s))
Tactic: rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)
have rw : Eq (α := ℝ) (List.sum (List.map (fun (x : ℝ) ↦ log x) (List.map (fun (i : α) ↦ f i) s.toList))) (∑ i ∈ s, log (f i))
Tactic: rw [← prod_map_toList, log_list_prod (by simp_all)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
Tactic: have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
Tactic: have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have simp : log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
  if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
    ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
  else 0
Tactic: simp only [finprod_def, finsum_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
have pos : ∀ (h' : HasFiniteMulSupport f),
  log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
Tactic: by_cases h' : HasFiniteMulSupport f
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
pos :
  ∀ (h' : HasFiniteMulSupport f),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
have neg : ∀ (h' : ¬HasFiniteMulSupport f),
  log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
Tactic: by_cases h' : HasFiniteMulSupport f
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have have : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
Tactic: classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
have : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have have₁ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
Tactic: classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
have : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₁ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₂ : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₃ have₄ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have have₅ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
  (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
  log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
Tactic: classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
have : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₁ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₂ : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₃ have₄ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₅ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
    log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have have₆ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
  (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
  log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
Tactic: classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
have : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₁ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₂ : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₃ have₄ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₅ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
    log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₆ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have pos : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
  (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)) (h' : HasFiniteMulSupport f),
  log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
Tactic: classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
have : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₁ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₂ : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₃ have₄ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₅ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
    log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₆ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
pos :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)) (h' : HasFiniteMulSupport f),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have neg : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
  (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)) (h' : ¬HasFiniteMulSupport f),
  log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
Tactic: classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
⊢ log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
have inl : log (↑0 : ℝ) = (Nat.factorization 0).sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
inl : log (↑0 : ℝ) = (Nat.factorization 0).sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
⊢ log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
have inr : ∀ (hn : n ≠ 0), log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
have inr : log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ log (↑(p ^ t) : ℝ)
Tactic: simp only [← log_pow, ← Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ log (↑(p ^ t) : ℝ)
have inr : ∀ (a : ℕ),
  Eq (α := ℝ) (↑(HPow.hPow (β := ℕ) a ((n.factorization : (a : ℕ) → ℕ) a : ℕ)) : ℝ) 0 →
    Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) a : ℕ) (0 : ℕ)
Tactic: rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.prod_factorization_pow_eq_self hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : Eq (α := ℝ) (↑(HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) : ℝ) 0
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr : Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
Tactic: rw [eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : Eq (α := ℝ) (↑(HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) : ℝ) 0
inr : Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr₁ : Eq (α := ℕ) 0 0
Tactic: rw [eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
a b : ℝ
n : ℕ
ha : a ≠ 0
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) fun (x : ℝ) ↦ log x ^ n / (a * x + b)
have h : ∀ (a_1 : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) x)
                  ((fun (x : ℝ) ↦ log x ^ n / (a * x + b)) x))
              x}
          x}
    a_1
Tactic: filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]