awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁)
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 < ε

Tactic:
⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩

Premises used: HDiv.hDiv, Metric.ball, Finset.prod, HAdd.hAdd, And.intro, Exists.intro, 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
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))
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 < ε
⊢ ∃ (t : Set R), (∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ t) ∧ ∀ x ∈ t, ∀ y ∈ t, dist x y < ε

Tactic:
refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ ε / 2 = r₁ * (ε / (2 * r₁))

Tactic:
field
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
refine_1 : ‖(∏ x ∈ s, (1 + f x)) * HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))
⊢ Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) (∏ x ∈ b, (1 + f x))

Tactic:
rw [← union_sdiff_of_subset hb, prod_union sdiff_disjoint.symm,
      Metric.mem_ball, dist_eq_norm_sub, ← mul_sub_one,
      show ε / 2 = r₁ * (ε / (2 * r₁)) by field]

Premises used: dist_eq_norm_sub, Finset.prod_union, mul_sub_one, Metric.mem_ball, Disjoint.symm, Finset.union_sdiff_of_subset, Finset.sdiff_disjoint
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
refine_1 :
  norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))
⊢ ‖(∏ x ∈ s, (1 + f x)) * HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))

Tactic:
apply (norm_mul_le _ _).trans_lt

Premises used: norm_mul_le, LE.le.trans_lt
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))

Tactic:
lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_

Premises used: lt_of_le_of_lt
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
refine_1 :
  norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ ≤
    r₁ * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖
refine_1₁ : r₁ * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))
⊢ norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))

Tactic:
refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_

Premises used: lt_of_le_of_lt
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ ≤
    r₁ * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖

Tactic:
mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
refine_1 : norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) ≤ r₁
⊢ norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ ≤
    r₁ * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) ≤ r₁

Tactic:
(Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)

Premises used: Finset.subset_union_left, LE.le.trans, Finset.norm_prod_le
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) ≤ r₁

Tactic:
exact (Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)

Premises used: Finset.subset_union_left, LE.le.trans, Finset.norm_prod_le
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ r₁ * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))

Tactic:
mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁

Premises used: mul_lt_mul_of_pos_left
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
refine_1 : Disjoint (b \ s) s₂
⊢ r₁ * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))

Tactic:
refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁

Premises used: mul_lt_mul_of_pos_left
-- 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₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ Disjoint (b \ s) s₂

Tactic:
simp [s, sdiff_union_distrib, disjoint_iff_inter_eq_empty]

Premises used: Finset.disjoint_iff_inter_eq_empty, Finset.sdiff_union_distrib
-- 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₁)
s : Finset ι := s₁ ∪ s₂
x : R
hx : Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) x
y : R
hy : Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) y
⊢ dist x y < ε

Tactic:
(dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)

Premises used: dist_triangle_right, Finset.prod, HAdd.hAdd, OfNat.ofNat, LE.le.trans_lt
-- 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₁)
s : Finset ι := s₁ ∪ s₂
x : R
hx : Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) x
y : R
hy : Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) y
⊢ dist x y < ε

Tactic:
exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)

Premises used: dist_triangle_right, Finset.prod, HAdd.hAdd, OfNat.ofNat, LE.le.trans_lt
-- 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‖
⊢ Summable.{u_2, u_1} (α := R) fun (s : Finset ι) ↦ ∏ i ∈ s, f i

Tactic:
(summable_finsetProd_of_summable_nonneg (fun _ ↦ norm_nonneg _) hf).of_norm_bounded
    fun _ ↦ Finset.norm_prod_le _ _

Premises used: Summable.of_norm_bounded, Finset.norm_prod_le, norm_nonneg, summable_finsetProd_of_summable_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
this : Summable (α := ℝ) fun (x : ι) ↦ ‖1 + f x‖ - 1
⊢ ∀ (b : ι), Real.log (1 + (‖1 + f b‖ - 1)) = Real.log ‖1 + f b‖

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
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
suffices : Summable (α := ℝ) fun (x : ι) ↦ ‖1 + f x‖ - 1
⊢ Summable (α := ℝ) fun (i : ι) ↦ Real.log ‖1 + f i‖

Tactic:
suffices Summable (‖1 + f ·‖ - 1) from
    (Real.summable_log_one_add_of_summable this).congr (by simp)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
⊢ 0 ≤ ‖‖1 + f i‖ - 1‖

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
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
refine : ∀ (i : ι), ‖‖1 + f i‖ - 1‖ ≤ ‖f i‖
⊢ Summable (α := ℝ) fun (x : ι) ↦ ‖1 + f x‖ - 1

Tactic:
refine .of_norm (hu.of_nonneg_of_le (fun i ↦ by positivity) fun i ↦ ?_)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
simp : -‖f i‖ ≤ ‖1 + f i‖ - 1 ∧ ‖1 + f i‖ - 1 ≤ ‖f i‖
⊢ ‖‖1 + f i‖ - 1‖ ≤ ‖f i‖

Tactic:
simp only [Real.norm_eq_abs, abs_le]

Premises used: abs_le, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
left : -‖f i‖ ≤ ‖1 + f i‖ - 1
right : ‖1 + f i‖ - 1 ≤ ‖f i‖
⊢ -‖f i‖ ≤ ‖1 + f i‖ - 1 ∧ ‖1 + f i‖ - 1 ≤ ‖f i‖

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
⊢ -‖f i‖ ≤ ‖1 + f i‖ - 1

Tactic:
simpa using norm_add_le (1 + f i) (-f i)

Premises used: norm_add_le, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
R : Type u_2
inst : NormedCommRing R
inst_1 : NormOneClass R
f : ι → R
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
⊢ ‖1 + f i‖ - 1 ≤ ‖f i‖

Tactic:
simpa [add_comm] using norm_add_le (f i) 1

Premises used: norm_add_le, add_comm, 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
inst_2 : CompleteSpace R
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
rw : Ne (α := ℝ) (∏' (i : ι), ‖1 + f i‖) 0
rw₁ : Multipliable.{u_2, u_1} (α := R) fun (i : ι) ↦ 1 + f i
⊢ Ne.{u_2 + 1} (α := R) (∏' (i : ι), (1 + f i)) 0

Tactic:
rw [← norm_ne_zero_iff, Multipliable.norm_tprod]

Premises used: Multipliable.norm_tprod, norm_ne_zero_iff
-- 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
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
rw : Real.exp (∑' (i : ι), Real.log ‖1 + f i‖) ≠ 0
⊢ Ne (α := ℝ) (∏' (i : ι), ‖1 + f i‖) 0

Tactic:
rw [← Real.rexp_tsum_eq_tprod (fun i ↦ norm_pos_iff.mpr <| hf i) hu.summable_log_norm_one_add]

Premises used: Iff.mpr, norm_pos_iff, Summable.summable_log_norm_one_add, Real.rexp_tsum_eq_tprod
-- 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
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
⊢ Real.exp (∑' (i : ι), Real.log ‖1 + f i‖) ≠ 0

Tactic:
apply Real.exp_ne_zero

Premises used: Real.exp_ne_zero
-- 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
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
⊢ Multipliable.{u_2, u_1} (α := R) fun (i : ι) ↦ 1 + f i

Tactic:
multipliable_one_add_of_summable hu

Premises used: multipliable_one_add_of_summable
-- 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
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
⊢ Multipliable.{u_2, u_1} (α := R) fun (i : ι) ↦ 1 + f i

Tactic:
exact multipliable_one_add_of_summable hu

Premises used: multipliable_one_add_of_summable
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε x : ℝ
⊢ ε.mulExpNegMulSq x = x * rexp (-(ε * x * x))

Tactic:
rfl

Premises used: Real.mulExpNegMulSq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε x : ℝ
⊢ -ε.mulExpNegMulSq (-x) = ε.mulExpNegMulSq x

Tactic:
simp [mulExpNegMulSq]

Premises used: Real.mulExpNegMulSq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
simp : x * rexp (-(x * x)) ≤ 1
⊢ mulExpNegMulSq 1 x ≤ 1

Tactic:
simp only [mulExpNegMulSq, one_mul]

Premises used: Real.mulExpNegMulSq, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
rw : x ≤ rexp (x * x)
⊢ x * rexp (-(x * x)) ≤ 1

Tactic:
rw [← le_div_iff₀ (exp_pos (-(x * x))), exp_neg, div_inv_eq_mul, one_mul]

Premises used: HMul.hMul, div_inv_eq_mul, le_div_iff₀, Real.exp_neg, Neg.neg, one_mul, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
apply : x ≤ x * x + 1
⊢ x ≤ rexp (x * x)

Tactic:
apply le_trans _ (add_one_le_exp (x * x))

Premises used: HMul.hMul, Real.add_one_le_exp, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
nlinarith :
  x * x + 1 < x →
    -1 + (0 - x * x) + 2 * (x * x + 1 - x) + (0 - (0 - x * x) * (0 - x * x)) + 2 * (0 - (0 - x * x) * (x * x + 1 - x)) +
        (0 - (x * x + 1 - x) * (x * x + 1 - x)) =
      0
nlinarith₁ nlinarith₂ : x * x + 1 < x → GT.gt (α := ℝ) 2 0
⊢ x ≤ x * x + 1

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
rw : mulExpNegMulSq 1 (-x) ≤ 1
⊢ -1 ≤ mulExpNegMulSq 1 x

Tactic:
rw [← neg_mulExpNegMulSq_neg, neg_le_neg_iff]

Premises used: Real.neg_mulExpNegMulSq_neg, neg_le_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
⊢ mulExpNegMulSq 1 (-x) ≤ 1

Tactic:
mulExpNegMulSq_one_le_one (-x)

Premises used: Real.mulExpNegMulSq_one_le_one, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
⊢ mulExpNegMulSq 1 (-x) ≤ 1

Tactic:
exact mulExpNegMulSq_one_le_one (-x)

Premises used: Real.mulExpNegMulSq_one_le_one, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
⊢ |mulExpNegMulSq 1 x| ≤ 1

Tactic:
abs_le.mpr ⟨neg_one_le_mulExpNegMulSq_one x, mulExpNegMulSq_one_le_one x⟩

Premises used: Iff.mpr, abs_le, And.intro, Real.neg_one_le_mulExpNegMulSq_one, Real.mulExpNegMulSq_one_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (-(ε * x * x))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
hf : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (x : α) ↦ ε.mulExpNegMulSq (f x)

Tactic:
continuous_mulExpNegMulSq.comp hf

Premises used: Continuous.comp, Real.mulExpNegMulSq, Real.continuous_mulExpNegMulSq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε y : ℝ
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ rexp (-(ε * x * x))) y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
⊢ Differentiable ℝ ε.mulExpNegMulSq

Tactic:
fun _ => differentiableAt_mulExpNegMulSq _

Premises used: Differentiable, Real.differentiableAt_mulExpNegMulSq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε y : ℝ
nth_rw : HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y
⊢ HasDerivAt ε.mulExpNegMulSq (rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
nth_rw 1 [← one_mul (exp (-(ε * y * y)))]

Premises used: HMul.hMul, Real.exp, Neg.neg, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε y : ℝ
apply : HasDerivAt (fun (x : ℝ) ↦ rexp (-(ε * x * x))) (rexp (-(ε * y * y)) * (-2 * ε * y)) y
⊢ HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
apply HasDerivAt.mul (hasDerivAt_id' y)

Premises used: hasDerivAt_id', HasDerivAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε y : ℝ
⊢ -(ε * 1 * y + ε * y * 1) = -2 * ε * y

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε y : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ rexp (-(ε * x * x))) (rexp (-(ε * y * y)) * (-2 * ε * y)) y

Tactic:
apply HasDerivAt.exp (HasDerivAt.congr_deriv (HasDerivAt.neg
    (HasDerivAt.mul (HasDerivAt.const_mul ε (hasDerivAt_id' y)) (hasDerivAt_id' y))) (by ring))

Premises used: hasDerivAt_id', HasDerivAt.neg, HasDerivAt.exp, HasDerivAt.const_mul, HasDerivAt.mul, HasDerivAt.congr_deriv
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε y : ℝ
⊢ deriv ε.mulExpNegMulSq y = rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))

Tactic:
HasDerivAt.deriv (hasDerivAt_mulExpNegMulSq y)

Premises used: HasDerivAt.deriv, Real.hasDerivAt_mulExpNegMulSq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
rw : |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ 1

Tactic:
rw [norm_eq_abs, deriv_mulExpNegMulSq]

Premises used: Real.deriv_mulExpNegMulSq, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))

Tactic:
have heq : exp (-(ε * x * x)) + x * (exp (-(ε * x * x)) * (-2 * ε * x))
      = exp (-(ε * x * x)) * (1 - 2 * (ε * x * x)) := by ring
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
rw : rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1

Tactic:
rw [heq, abs_mul, abs_exp]

Premises used: abs_mul, Real.abs_exp