awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
T : Finset (Finset ι)
⊢ ∏ i ∈ T.biUnion id, (1 + f i) ≤ Real.exp (∑ i ∈ T.biUnion id, f i)

Tactic:
Real.prod_one_add_le_exp_sum _ hf

Premises used: Real.prod_one_add_le_exp_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
T : Finset (Finset ι)
⊢ Real.exp (∑ i ∈ T.biUnion id, f i) ≤ Real.exp (∑' (i : ι), f i)

Tactic:
Real.exp_le_exp.mpr (hfs.sum_le_tsum _ fun _ _ ↦ hf _)

Premises used: Iff.mpr, Summable.sum_le_tsum, Real.exp_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
T : Finset (Finset ι)
⊢ ∑ x ∈ T, ∏ i ∈ x, f i ≤ Real.exp (∑' (i : ι), f i)

Tactic:
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 _)

Premises used: Iff.mpr, Real.prod_one_add_le_exp_sum, id, Finset.prod_one_add, Finset.biUnion, Real.exp, Finset.mem_powerset, Finset.subset_biUnion_of_mem, Summable.sum_le_tsum, Real.exp_le_exp, tsum, Finset.powerset, Finset.sum_le_sum_of_subset_of_nonneg, Eq.symm, Finset.sum, Finset.prod_nonneg, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
refine : ∀ (T : Finset (Finset ι)), ∑ x ∈ T, ∏ i ∈ x, f i ≤ Real.exp (∑' (i : ι), f i)
⊢ Summable (α := ℝ) fun (s : Finset ι) ↦ ∏ i ∈ s, 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 _)

Premises used: Iff.mpr, Real.prod_one_add_le_exp_sum, id, Finset.prod_one_add, Real.exp, Finset.mem_powerset, Finset.subset_biUnion_of_mem, Summable.sum_le_tsum, Real.exp_le_exp, tsum, summable_of_sum_le, Finset.sum_le_sum_of_subset_of_nonneg, Eq.symm, Finset.prod_nonneg, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
obtain :
  ∀ (r₁ : ℝ) (hr₁ : max 0 (∏' (i : ι), v i) < r₁),
    ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, 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)

Premises used: NoMaxOrder.exists_gt, Max.max, tprod, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : max 0 (∏' (i : ι), v i) < r₁
⊢ 0 < r₁ ∧ ∏' (i : ι), v i < r₁

Tactic:
rw [max_lt_iff] at hr₁

Premises used: max_lt_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
⊢ ∀ᶠ (a : Finset ι) in (unconditional ι).filter, ∏ b ∈ a, v b ≤ r₁

Tactic:
have := hv.hasProd.eventually_le_const hr₁.2
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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₁
⊢ ∃ (a : Finset ι), ∀ b ≥ a, ∏ b ∈ b, v b ≤ r₁

Tactic:
rw [unconditional, eventually_atTop] at this

Premises used: Filter.eventually_atTop, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∃ (a : Finset ι), ∀ b ≥ a, ∏ b ∈ b, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
⟨r₁, hr₁.1, this⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∃ (a : Finset ι), ∀ b ≥ a, ∏ b ∈ b, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
exact ⟨r₁, hr₁.1, this⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
h : ∀ (i : ι), ‖1 + f i‖
| Multipliable (α := ℝ) fun (i : ι) ↦ ‖1 + f i‖

Tactic:
enter [1, i]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
i : ι
h : 1 + (‖1 + f i‖ - 1)
| ‖1 + f i‖

Tactic:
rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]

Premises used: Norm.norm, add_comm, HAdd.hAdd, OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
h : ∀ (i : ι), 1 + (‖1 + f i‖ - 1)
| Multipliable (α := ℝ) fun (i : ι) ↦ ‖1 + f i‖

Tactic:
enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
conv : Multipliable (α := ℝ) fun (i : ι) ↦ 1 + (‖1 + f i‖ - 1)
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ ‖1 + f i‖

Tactic:
conv => enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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)

Tactic:
Real.multipliable_one_add_of_summable <| hf.of_norm_bounded (fun i ↦ ?_)

Premises used: Real.multipliable_one_add_of_summable, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
refine : ∀ (i : ι), ‖‖1 + f i‖ - 1‖ ≤ ‖f i‖
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ 1 + (‖1 + f i‖ - 1)

Tactic:
refine Real.multipliable_one_add_of_summable <| hf.of_norm_bounded (fun i ↦ ?_)

Premises used: Real.multipliable_one_add_of_summable, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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‖ - 1‖ ≤ ‖f i‖

Tactic:
simpa using abs_norm_sub_norm_le (1 + f i) 1

Premises used: abs_norm_sub_norm_le, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
⊢ ‖HSub.hSub (α := R) (∏ i ∈ ∅, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ ∅, ‖f i‖) - 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
⊢ (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 = HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1 + f x * ∏ x ∈ t, (1 + f x)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
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
⊢ ‖HSub.hSub (α := R) (∏ i ∈ Insert.insert x t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ Insert.insert x t, ‖f i‖) - 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]

Premises used: Finset.prod_insert, Finset.sum_insert, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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

Tactic:
(norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_

Premises used: norm_add_le_of_le, LE.le.trans, norm_mul_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
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
⊢ ‖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:
refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_

Premises used: norm_add_le_of_le, LE.le.trans, norm_mul_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
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
⊢ 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:
generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH

Premises used: Norm.norm, Real.exp, Finset.sum
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
insert : A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A
⊢ A - 1 + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A - 1

Tactic:
rw [sub_add_eq_add_sub, sub_le_sub_iff_right]

Premises used: sub_le_sub_iff_right, sub_add_eq_add_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
transitivity₁ : A + ‖f x‖ * A ≤ Real.exp ‖f x‖ * A
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ Real.exp ‖f x‖ * A

Tactic:
transitivity A + ‖f x‖ * A
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
grw₃ grw₄ : A + ‖f x‖ * A ≤ A + ‖f x‖ * A
⊢ A + ‖f x‖ * norm.{u_2} (E := R) (∏ x ∈ t, (1 + f x)) ≤ A + ‖f x‖ * A

Tactic:
grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]

Premises used: NormOneClass.norm_one, Finset.prod, norm_le_norm_sub_add, HAdd.hAdd, OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
rw : (‖f x‖ + 1) * A ≤ Real.exp ‖f x‖ * A
⊢ A + ‖f x‖ * A ≤ Real.exp ‖f x‖ * A

Tactic:
rw [← one_add_mul, add_comm]

Premises used: add_comm, one_add_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
⊢ (‖f x‖ + 1) * A ≤ Real.exp ‖f x‖ * A

Tactic:
mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, Real.add_one_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
⊢ (‖f x‖ + 1) * A ≤ Real.exp ‖f x‖ * A

Tactic:
exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, Real.add_one_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
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.insert x t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ Insert.insert x t, ‖f i‖) - 1
⊢ ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ 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 _)

Premises used: Norm.norm, NormOneClass.norm_one, sub_le_sub_iff_right, Insert.insert, Real.exp, add_comm, Finset.prod, norm_le_norm_sub_add, mul_le_mul_of_nonneg_right, HAdd.hAdd, one_add_mul, OfNat.ofNat, sub_add_eq_add_sub, Real.add_one_le_exp, sub_add_cancel, Finset.sum, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
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.insert x t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ Insert.insert x t, ‖f i‖) - 1
⊢ ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + f i)) 1‖ ≤ Real.exp (∑ i ∈ 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 _)

Premises used: Norm.norm, NormOneClass.norm_one, sub_le_sub_iff_right, Insert.insert, Real.exp, add_comm, Finset.prod, norm_le_norm_sub_add, mul_le_mul_of_nonneg_right, HAdd.hAdd, one_add_mul, OfNat.ofNat, sub_add_eq_add_sub, Real.add_one_le_exp, sub_add_cancel, Finset.sum, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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 < ε
suffices : ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → Real.exp (∑ i ∈ t, ‖f i‖) - 1 < ε
⊢ ∃ (s₂ : Finset ι), ∀ (t : Finset ι), Disjoint t s₂ → ‖HSub.hSub (α := R) (∏ i ∈ t, (1 + 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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 < ε
suffices : Membership.mem (γ := Filter ℝ) (𝓝 0) {x : ℝ | Real.exp x - 1 < ε}
⊢ ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → Real.exp (∑ i ∈ t, ‖f i‖) - 1 < ε

Tactic:
suffices {x | Real.exp x - 1 < ε} ∈ 𝓝 0 from hf.vanishing this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
⊢ Set.Iio ε ∈ 𝓝 (f 0)

Tactic:
simpa [f] using Iio_mem_nhds hε

Premises used: Iio_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
⊢ Set.Iio ε ∈ 𝓝 (f 0)

Tactic:
have : Set.Iio ε ∈ nhds (f 0) := by simpa [f] using Iio_mem_nhds hε
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
this : Set.Iio ε ∈ 𝓝 (f 0)
⊢ ContinuousAt f 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
this : Set.Iio ε ∈ 𝓝 (f 0)
⊢ Membership.mem (γ := Filter ℝ) (𝓝 0) {x : ℝ | Real.exp x - 1 < ε}

Tactic:
exact ContinuousAt.preimage_mem_nhds (by fun_prop) this

Premises used: ContinuousAt.preimage_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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‖
⊢ Filter.NeBot.{u_2} (α := R)
    (Filter.map (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (i : ι) ↦ 1 + f i) b) (unconditional ι).filter)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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‖
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 < ε
⊢ Multipliable.{u_2, u_1} (α := R) fun (i : ι) ↦ 1 + f i

Tactic:
refine CompleteSpace.complete <| Metric.cauchy_iff.mpr ⟨by infer_instance, fun ε hε ↦ ?_⟩

Premises used: Iff.mpr, Metric.cauchy_iff, CompleteSpace.complete, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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
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 < ε
⊢ ∃ (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

Premises used: multipliable_norm_one_add_of_summable_norm, Multipliable.eventually_bounded_finsetProd
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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₁
⊢ 0 < ε / (2 * r₁)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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₁
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 < ε
⊢ ∃ (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)

Premises used: prod_vanishing_of_summable_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
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₁)
simp :
  ∃ (t : Set R), (∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ t) ∧ ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
⊢ ∃ (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:
simp only [unconditional, Filter.mem_map, mem_atTop_sets, ge_iff_le, le_eq_subset,
    Set.mem_preimage]

Premises used: ge_iff_le, Filter.mem_atTop_sets, Finset.le_eq_subset, Filter.mem_map, Set.mem_preimage, SummationFilter.unconditional