awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
i : ι
hi : -1 ≤ f i
⊢ 0 ≤ 1 + f i
have linarith : 1 + f i < 0 → -1 - f i + (1 + f i - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ 1 + f i
have refine : ∀ᶠ (i : ι) in cofinite, 0 < 1 + f i
Tactic: refine multipliable_of_summable_log' ?_ (summable_log_one_add_of_summable hf)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ ∀ᶠ (i : ι) in cofinite, 0 < 1 + f i
have h : ∀ (i : ι) (hi : -1 < f i), 0 < 1 + f i
Tactic: filter_upwards [hf.tendsto_cofinite_zero.eventually_const_lt neg_one_lt_zero] with i hi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
i : ι
hi : -1 < f i
⊢ 0 < 1 + f i
have linarith : 1 + f i ≤ 0 → -1 - f i + (1 + f i - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
⊢ Summable (α := ℝ) fun (s : Finset ι) ↦ ∏ i ∈ s, f i
have refine : ∀ (T : Finset (Finset ι)), ∑ x ∈ T, ∏ i ∈ x, f i ≤ Real.exp (∑' (i : ι), f i)
Tactic: refine summable_of_sum_le (c := Real.exp (∑' i, f i))
    (fun s ↦ Finset.prod_nonneg fun i _ ↦ hf i) fun T ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
⊢ Summable (α := ℝ) fun (s : Finset ι) ↦ ∏ i ∈ s, f i
have refine : ∀ (T : Finset (Finset ι)), ∑ x ∈ T, ∏ i ∈ x, f i ≤ Real.exp (∑' (i : ι), f i)
Tactic: classical
  refine summable_of_sum_le (c := Real.exp (∑' i, f i))
    (fun s ↦ Finset.prod_nonneg fun i _ ↦ hf i) fun T ↦ ?_
  calc ∑ s ∈ T, ∏ i ∈ s, f i
      ≤ ∑ s ∈ (T.biUnion id).powerset, ∏ i ∈ s, f i :=
        Finset.sum_le_sum_of_subset_of_nonneg (fun s hs ↦ Finset.mem_powerset.mpr
          (Finset.subset_biUnion_of_mem id hs)) (fun s _ _ ↦ Finset.prod_nonneg fun i _ ↦ hf i)
    _ = ∏ i ∈ T.biUnion id, (1 + f i) := (Finset.prod_one_add _).symm
    _ ≤ Real.exp (∑ i ∈ T.biUnion id, f i) := Real.prod_one_add_le_exp_sum _ hf
    _ ≤ Real.exp (∑' i, f i) :=
        Real.exp_le_exp.mpr (hfs.sum_le_tsum _ fun _ _ ↦ hf _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
⊢ ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
have obtain : ∀ (r₁ : ℝ) (hr₁ : max 0 (∏' (i : ι), v i) < r₁),
  ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
Tactic: obtain ⟨r₁, hr₁⟩ := exists_gt (max 0 <| ∏' i, v i)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (hypothesis)
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : max 0 (∏' (i : ι), v i) < r₁
⊢ ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
have hr₂ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
Tactic: rw [max_lt_iff] at hr₁
Cleared hypotheses: hr₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (hypothesis)
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
⊢ ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
have this : ∀ᶠ (a : Finset ι) in (unconditional ι).filter, ∏ b ∈ a, v b ≤ r₁
Tactic: have := hv.hasProd.eventually_le_const hr₁.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (hypothesis)
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∀ᶠ (a : Finset ι) in (unconditional ι).filter, ∏ b ∈ a, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
have this₁ : ∃ (a : Finset ι), ∀ b ≥ a, ∏ b ∈ b, v b ≤ r₁
Tactic: rw [unconditional, eventually_atTop] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
| Multipliable (α := ℝ) fun (i : ι) ↦ ‖1 + f i‖
have h : ∀ (i : ι), ‖1 + f i‖
Tactic: enter [1, i]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
i : ι
| ‖1 + f i‖
have h : 1 + (‖1 + f i‖ - 1)
Tactic: rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
| Multipliable (α := ℝ) fun (i : ι) ↦ ‖1 + f i‖
have h : ∀ (i : ι), 1 + (‖1 + f i‖ - 1)
Tactic: enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ ‖1 + f i‖
have conv : Multipliable (α := ℝ) fun (i : ι) ↦ 1 + (‖1 + f i‖ - 1)
Tactic: conv => enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ 1 + (‖1 + f i‖ - 1)
have refine : ∀ (i : ι), ‖‖1 + f i‖ - 1‖ ≤ ‖f i‖
Tactic: refine Real.multipliable_one_add_of_summable <| hf.of_norm_bounded (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
⊢ ‖HSub.hSub (α := R) (∏ i ∈ insert x t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ insert x t, ‖f i‖) - 1
have insert : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1 + f x * ∏ x ∈ t, (1 + f x)‖ ≤ Real.exp ‖f x‖ * Real.exp (∑ x ∈ t, ‖f x‖) - 1
Tactic: rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
      show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
⊢ ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1 + f x * ∏ x ∈ t, (1 + f x)‖ ≤
    Real.exp ‖f x‖ * Real.exp (∑ x ∈ t, ‖f x‖) - 1
have insert : Real.exp (∑ i ∈ t, ‖f i‖) - 1 + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤
  Real.exp ‖f x‖ * Real.exp (∑ x ∈ t, ‖f x‖) - 1
Tactic: refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
⊢ Real.exp (∑ i ∈ t, ‖f i‖) - 1 + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤
    Real.exp ‖f x‖ * Real.exp (∑ x ∈ t, ‖f x‖) - 1
have insert : ∀ (A : ℝ) (h : Real.exp (∑ i ∈ t, ‖f i‖) = A) (IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1),
  A - 1 + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A - 1
Tactic: generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
⊢ A - 1 + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A - 1
have insert : A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A
Tactic: rw [sub_add_eq_add_sub, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A
have transitivity : A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A
Tactic: transitivity A + ‖f x‖ * A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
transitivity : A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A
have transitivity₁ : A + ‖f x‖ * A ≤ Real.exp ‖f x‖ * A
Tactic: transitivity A + ‖f x‖ * A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A
have h₁ : 0 ≤ ‖f x‖
Tactic: grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
h₁ : 0 ≤ ‖f x‖
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A
have grw : A + ‖f x‖ * (‖HSub.hSub (α := R) (∏ x ∈ t, (1 + f x)) 1‖ + norm.{u_2} (E := R) 1) ≤ A + ‖f x‖ * A
Tactic: grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
h₁ : 0 ≤ ‖f x‖
grw : A + ‖f x‖ * (‖HSub.hSub (α := R) (∏ x ∈ t, (1 + f x)) 1‖ + norm.{u_2} (E := R) 1) ≤ A + ‖f x‖ * A
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A
have grw₁ : A + ‖f x‖ * (A - 1 + norm.{u_2} (E := R) 1) ≤ A + ‖f x‖ * A
Tactic: grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
h₁ : 0 ≤ ‖f x‖
grw : A + ‖f x‖ * (‖HSub.hSub (α := R) (∏ x ∈ t, (1 + f x)) 1‖ + norm.{u_2} (E := R) 1) ≤ A + ‖f x‖ * A
grw₁ : A + ‖f x‖ * (A - 1 + norm.{u_2} (E := R) 1) ≤ A + ‖f x‖ * A
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A
have grw₂ : A + ‖f x‖ * (A - 1 + 1) ≤ A + ‖f x‖ * A
Tactic: grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
h₁ : 0 ≤ ‖f x‖
grw : A + ‖f x‖ * (‖HSub.hSub (α := R) (∏ x ∈ t, (1 + f x)) 1‖ + norm.{u_2} (E := R) 1) ≤ A + ‖f x‖ * A
grw₁ : A + ‖f x‖ * (A - 1 + norm.{u_2} (E := R) 1) ≤ A + ‖f x‖ * A
grw₂ : A + ‖f x‖ * (A - 1 + 1) ≤ A + ‖f x‖ * A
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A
have grw₃ : A + ‖f x‖ * A ≤ A + ‖f x‖ * A
Tactic: grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ A - 1
⊢ A + ‖f x‖ * A ≤ Real.exp ‖f x‖ * A
have rw : (‖f x‖ + 1) * A ≤ Real.exp ‖f x‖ * A
Tactic: rw [← one_add_mul, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
t : Finset ι
f : ι → R
⊢ ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
have empty : ‖HSub.hSub (α := R) (∏ i ∈ ∅, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ ∅, ‖f i‖) - 1
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert x t hx IH =>
    rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
      show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]
    refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_
    generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH
    rw [sub_add_eq_add_sub, sub_le_sub_iff_right]
    transitivity A + ‖f x‖ * A
    · grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
    rw [← one_add_mul, add_comm]
    exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
t : Finset ι
f : ι → R
empty : ‖HSub.hSub (α := R) (∏ i ∈ ∅, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ ∅, ‖f i‖) - 1
⊢ ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
have insert : ∀ (x : ι) (t : Finset ι) (hx : x ∉ t)
  (IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1),
  ‖HSub.hSub (α := R) (∏ i ∈ insert x t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ insert x t, ‖f i‖) - 1
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert x t hx IH =>
    rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
      show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]
    refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_
    generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH
    rw [sub_add_eq_add_sub, sub_le_sub_iff_right]
    transitivity A + ‖f x‖ * A
    · grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
    rw [← one_add_mul, add_comm]
    exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
t : Finset ι
f : ι → R
⊢ ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
have empty : ‖HSub.hSub (α := R) (∏ i ∈ ∅, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ ∅, ‖f i‖) - 1
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert x t hx IH =>
    rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
      show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]
    refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_
    generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH
    rw [sub_add_eq_add_sub, sub_le_sub_iff_right]
    transitivity A + ‖f x‖ * A
    · grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
    rw [← one_add_mul, add_comm]
    exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
t : Finset ι
f : ι → R
empty : ‖HSub.hSub (α := R) (∏ i ∈ ∅, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ ∅, ‖f i‖) - 1
⊢ ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
have insert : ∀ (x : ι) (t : Finset ι) (hx : x ∉ t)
  (IH : ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1),
  ‖HSub.hSub (α := R) (∏ i ∈ insert x t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ insert x t, ‖f i‖) - 1
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert x t hx IH =>
    rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
      show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]
    refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_
    generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH
    rw [sub_add_eq_add_sub, sub_le_sub_iff_right]
    transitivity A + ‖f x‖ * A
    · grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
    rw [← one_add_mul, add_comm]
    exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
ε : ℝ
hε : 0 < ε
⊢ ∃ (s₂ : Finset ι), ∀ (t : Finset ι), Disjoint t s₂ → ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ < ε
have suffices : ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → Real.exp (∑ i ∈ t, ‖f i‖) - 1 < ε
Tactic: suffices ∃ s, ∀ t, Disjoint t s → Real.exp (∑ i ∈ t, ‖f i‖) - 1 < ε from
    this.imp fun s hs t ht ↦ (t.norm_prod_one_add_sub_one_le _).trans_lt (hs t ht)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
ε : ℝ
hε : 0 < ε
⊢ ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → Real.exp (∑ i ∈ t, ‖f i‖) - 1 < ε
have suffices : Membership.mem (γ := Filter ℝ) (𝓝 0) {x : ℝ | Real.exp x - 1 < ε}
Tactic: suffices {x | Real.exp x - 1 < ε} ∈ 𝓝 0 from hf.vanishing this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f_1 : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f_1 i‖
ε : ℝ
hε : 0 < ε
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ Real.exp x - 1
⊢ Membership.mem (γ := Filter ℝ) (𝓝 0) {x : ℝ | Real.exp x - 1 < ε}
have this : Set.Iio ε ∈ 𝓝 (f 0)
Tactic: have : Set.Iio ε ∈ nhds (f 0) := by simpa [f] using Iio_mem_nhds hε
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
inst_2 : CompleteSpace R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
⊢ Multipliable.{u_2, u_1} (α := R) fun (i : ι) ↦ 1 + f i
have refine : ∀ (ε : ℝ) (hε : ε > 0),
  ∃ (t : Set R),
    Membership.mem (γ := Filter R)
        (Filter.map (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (i : ι) ↦ 1 + f i) b) (unconditional ι).filter) t ∧
      ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
Tactic: refine CompleteSpace.complete <| Metric.cauchy_iff.mpr ⟨by infer_instance, fun ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
inst_2 : CompleteSpace R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
ε : ℝ
hε : ε > 0
⊢ ∃ (t : Set R),
    Membership.mem (γ := Filter R)
        (Filter.map (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (i : ι) ↦ 1 + f i) b) (unconditional ι).filter) t ∧
      ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
have obtain : ∀ (r₁ : ℝ) (hr₁ : r₁ > 0) (s₁ : Finset ι) (hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁),
  ∃ (t : Set R),
    Membership.mem (γ := Filter R)
        (Filter.map (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (i : ι) ↦ 1 + f i) b) (unconditional ι).filter) t ∧
      ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
Tactic: obtain ⟨r₁, hr₁, s₁, hs₁⟩ :=
    (multipliable_norm_one_add_of_summable_norm hf).eventually_bounded_finsetProd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
inst_2 : CompleteSpace R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
⊢ ∃ (t : Set R),
    Membership.mem (γ := Filter R)
        (Filter.map (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (i : ι) ↦ 1 + f i) b) (unconditional ι).filter) t ∧
      ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
have obtain : ∀ (s₂ : Finset ι) (hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ < ε / (2 * r₁)),
  ∃ (t : Set R),
    Membership.mem (γ := Filter R)
        (Filter.map (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (i : ι) ↦ 1 + f i) b) (unconditional ι).filter) t ∧
      ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
Tactic: obtain ⟨s₂, hs₂⟩ := prod_vanishing_of_summable_norm hf (show 0 < ε / (2 * r₁) by positivity)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
inst_2 : CompleteSpace R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ < ε / (2 * r₁)
⊢ ∃ (t : Set R),
    Membership.mem (γ := Filter R)
        (Filter.map (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (i : ι) ↦ 1 + f i) b) (unconditional ι).filter) t ∧
      ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
have simp : ∃ (t : Set R), (∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ t) ∧ ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
Tactic: simp only [unconditional, Filter.mem_map, mem_atTop_sets, ge_iff_le, le_eq_subset,
    Set.mem_preimage]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
inst_2 : CompleteSpace R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
⊢ ∃ (t : Set R), (∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ t) ∧ ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
have refine_1 : ∀ (b : Finset ι) (hb : s ⊆ b),
  Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) (∏ x ∈ b, (1 + f x))
Tactic: refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
inst_2 : CompleteSpace R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
refine_1 :
  ∀ (b : Finset ι) (hb : s ⊆ b),
    Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) (∏ x ∈ b, (1 + f x))
⊢ ∃ (t : Set R), (∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ t) ∧ ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
have refine_2 : ∀ (x : R),
  Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) x →
    ∀ (y : R), Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) y → dist x y < ε
Tactic: refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩