awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
b : Finset ι
hb : s ⊆ b
⊢ Membership.mem (γ := Set R) (Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)) (∏ x ∈ b, (1 + f x))
have refine_1 : ‖(∏ x ∈ s, (1 + f x)) * HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))
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]
-- 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₂
b : Finset ι
hb : s ⊆ b
⊢ ‖(∏ x ∈ s, (1 + f x)) * HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))
have 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₁))
Tactic: apply (norm_mul_le _ _).trans_lt
-- 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₂
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₁))
have 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‖
Tactic: refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_
-- 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₂
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‖
⊢ norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))
have refine_1₁ : r₁ * ‖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‖) ?_ ?_
-- 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₂
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‖
have refine_1 : norm.{u_2} (E := R) (∏ x ∈ s, (1 + f x)) ≤ r₁
Tactic: refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
-- 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₂
b : Finset ι
hb : s ⊆ b
⊢ r₁ * ‖HSub.hSub (α := R) (∏ x ∈ b \ s, (1 + f x)) 1‖ < r₁ * (ε / (2 * r₁))
have refine_1 : Disjoint (b \ s) s₂
Tactic: refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁
-- 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: classical
  refine CompleteSpace.complete <| Metric.cauchy_iff.mpr ⟨by infer_instance, fun ε hε ↦ ?_⟩
  obtain ⟨r₁, hr₁, s₁, hs₁⟩ :=
    (multipliable_norm_one_add_of_summable_norm hf).eventually_bounded_finsetProd
  obtain ⟨s₂, hs₂⟩ := prod_vanishing_of_summable_norm hf (show 0 < ε / (2 * r₁) by positivity)
  simp only [unconditional, Filter.mem_map, mem_atTop_sets, ge_iff_le, le_eq_subset,
    Set.mem_preimage]
  let s := s₁ ∪ s₂
  -- The idea here is that if `s` is a large enough finset, then the product over `s` is bounded
  -- by some `r`, and the product over finsets disjoint from `s` is within `ε / (2 * r)` of 1.
  -- From this it follows that the products over any two finsets containing `s` are within `ε` of
  -- each other.
  -- Here `s₁ ⊆ s` guarantees that the product over `s` is bounded, and `s₂ ⊆ s` guarantees that
  -- the product over terms not in `s` is small.
  refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩
  · 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]
    apply (norm_mul_le _ _).trans_lt
    refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_
    · refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      exact (Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)
    · refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁
      simp [s, sdiff_union_distrib, disjoint_iff_inter_eq_empty]
  · intro x hx y hy
    exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)
-- 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‖
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
have refine₁ : ∀ (ε : ℝ) (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 < ε
Tactic: classical
  refine CompleteSpace.complete <| Metric.cauchy_iff.mpr ⟨by infer_instance, fun ε hε ↦ ?_⟩
  obtain ⟨r₁, hr₁, s₁, hs₁⟩ :=
    (multipliable_norm_one_add_of_summable_norm hf).eventually_bounded_finsetProd
  obtain ⟨s₂, hs₂⟩ := prod_vanishing_of_summable_norm hf (show 0 < ε / (2 * r₁) by positivity)
  simp only [unconditional, Filter.mem_map, mem_atTop_sets, ge_iff_le, le_eq_subset,
    Set.mem_preimage]
  let s := s₁ ∪ s₂
  -- The idea here is that if `s` is a large enough finset, then the product over `s` is bounded
  -- by some `r`, and the product over finsets disjoint from `s` is within `ε / (2 * r)` of 1.
  -- From this it follows that the products over any two finsets containing `s` are within `ε` of
  -- each other.
  -- Here `s₁ ⊆ s` guarantees that the product over `s` is bounded, and `s₂ ⊆ s` guarantees that
  -- the product over terms not in `s` is small.
  refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩
  · 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]
    apply (norm_mul_le _ _).trans_lt
    refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_
    · refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      exact (Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)
    · refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁
      simp [s, sdiff_union_distrib, disjoint_iff_inter_eq_empty]
  · intro x hx y hy
    exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)
-- 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‖
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 < ε
refine₁ :
  ∀ (ε : ℝ) (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 < ε
⊢ Multipliable.{u_2, u_1} (α := R) fun (i : ι) ↦ 1 + f i
have refine₂ : ∀ (ε : ℝ) (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 < ε
Tactic: classical
  refine CompleteSpace.complete <| Metric.cauchy_iff.mpr ⟨by infer_instance, fun ε hε ↦ ?_⟩
  obtain ⟨r₁, hr₁, s₁, hs₁⟩ :=
    (multipliable_norm_one_add_of_summable_norm hf).eventually_bounded_finsetProd
  obtain ⟨s₂, hs₂⟩ := prod_vanishing_of_summable_norm hf (show 0 < ε / (2 * r₁) by positivity)
  simp only [unconditional, Filter.mem_map, mem_atTop_sets, ge_iff_le, le_eq_subset,
    Set.mem_preimage]
  let s := s₁ ∪ s₂
  -- The idea here is that if `s` is a large enough finset, then the product over `s` is bounded
  -- by some `r`, and the product over finsets disjoint from `s` is within `ε / (2 * r)` of 1.
  -- From this it follows that the products over any two finsets containing `s` are within `ε` of
  -- each other.
  -- Here `s₁ ⊆ s` guarantees that the product over `s` is bounded, and `s₂ ⊆ s` guarantees that
  -- the product over terms not in `s` is small.
  refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩
  · 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]
    apply (norm_mul_le _ _).trans_lt
    refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_
    · refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      exact (Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)
    · refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁
      simp [s, sdiff_union_distrib, disjoint_iff_inter_eq_empty]
  · intro x hx y hy
    exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)
-- 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
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
⊢ Summable (α := ℝ) fun (i : ι) ↦ Real.log ‖1 + f i‖
have suffices : Summable (α := ℝ) fun (x : ι) ↦ ‖1 + f x‖ - 1
Tactic: suffices Summable (‖1 + f ·‖ - 1) from
    (Real.summable_log_one_add_of_summable this).congr (by simp)
-- 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
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
⊢ Summable (α := ℝ) fun (x : ι) ↦ ‖1 + f x‖ - 1
have refine : ∀ (i : ι), ‖‖1 + f i‖ - 1‖ ≤ ‖f i‖
Tactic: refine .of_norm (hu.of_nonneg_of_le (fun i ↦ by positivity) 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
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
⊢ ‖‖1 + f i‖ - 1‖ ≤ ‖f i‖
have simp : -‖f i‖ ≤ ‖1 + f i‖ - 1 ∧ ‖1 + f i‖ - 1 ≤ ‖f i‖
Tactic: simp only [Real.norm_eq_abs, abs_le]
-- 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
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
⊢ -‖f i‖ ≤ ‖1 + f i‖ - 1 ∧ ‖1 + f i‖ - 1 ≤ ‖f i‖
have left : -‖f i‖ ≤ ‖1 + f i‖ - 1
Tactic: constructor
-- 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
hu : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
i : ι
left : -‖f i‖ ≤ ‖1 + f i‖ - 1
⊢ -‖f i‖ ≤ ‖1 + f i‖ - 1 ∧ ‖1 + f i‖ - 1 ≤ ‖f i‖
have right : ‖1 + f i‖ - 1 ≤ ‖f i‖
Tactic: constructor
-- 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
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
⊢ Ne.{u_2 + 1} (α := R) (∏' (i : ι), (1 + f i)) 0
have rw : Ne (α := ℝ) (∏' (i : ι), ‖1 + f i‖) 0
Tactic: rw [← norm_ne_zero_iff, Multipliable.norm_tprod]
-- 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
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
rw : Ne (α := ℝ) (∏' (i : ι), ‖1 + f i‖) 0
⊢ Ne.{u_2 + 1} (α := R) (∏' (i : ι), (1 + f i)) 0
have rw₁ : Multipliable.{u_2, u_1} (α := R) fun (i : ι) ↦ 1 + f i
Tactic: rw [← norm_ne_zero_iff, Multipliable.norm_tprod]
-- 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
inst_3 : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
⊢ Ne (α := ℝ) (∏' (i : ι), ‖1 + f i‖) 0
have rw : Real.exp (∑' (i : ι), Real.log ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
x : ℝ
⊢ mulExpNegMulSq 1 x ≤ 1
have simp : x * rexp (-(x * x)) ≤ 1
Tactic: simp only [mulExpNegMulSq, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
x : ℝ
⊢ x * rexp (-(x * x)) ≤ 1
have rw : x ≤ rexp (x * x)
Tactic: rw [← le_div_iff₀ (exp_pos (-(x * x))), exp_neg, div_inv_eq_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
x : ℝ
⊢ x ≤ rexp (x * x)
have apply : x ≤ x * x + 1
Tactic: apply le_trans _ (add_one_le_exp (x * x))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
x : ℝ
⊢ x ≤ x * x + 1
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
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
⊢ x ≤ x * x + 1
have nlinarith₁ : x * x + 1 < x → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
x : ℝ
⊢ -1 ≤ mulExpNegMulSq 1 x
have rw : mulExpNegMulSq 1 (-x) ≤ 1
Tactic: rw [← neg_mulExpNegMulSq_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y
have nth_rw : HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y
Tactic: nth_rw 1 [← one_mul (exp (-(ε * y * y)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y
have apply : HasDerivAt (fun (x : ℝ) ↦ rexp (-(ε * x * x))) (rexp (-(ε * y * y)) * (-2 * ε * y)) y
Tactic: apply HasDerivAt.mul (hasDerivAt_id' y)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ 1
have rw : |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1
Tactic: rw [norm_eq_abs, deriv_mulExpNegMulSq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (hypothesis)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1
have heq : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1
have rw : rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1
Tactic: rw [heq, abs_mul, abs_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1
have set : let y := ε * x * x;
∀ (heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)) (hy : y = ε * x * x),
  rexp (-y) * |1 - 2 * y| ≤ 1
Tactic: set y := ε * x * x with hy
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ y
have rw : 0 ≤ ε * (x * x)
Tactic: rw [hy, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (hypothesis)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ rexp (-y) * |1 - 2 * y| ≤ 1
have hynonneg : 0 ≤ y
Tactic: have hynonneg : 0 ≤ y := by
    rw [hy, mul_assoc]
    exact mul_nonneg hε.le (mul_self_nonneg x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ rexp (-y) * |1 - 2 * y| ≤ 1
have apply : |1 - 2 * y| ≤ (rexp (-y))⁻¹ * 1
Tactic: apply mul_le_of_le_inv_mul₀ (zero_le_one' ℝ) (exp_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ |1 - 2 * y| ≤ (rexp (-y))⁻¹ * 1
have simp : 2 * y ≤ 1 + rexp y ∧ 1 ≤ rexp y + 2 * y
Tactic: simp only [← exp_neg (-y), neg_neg, mul_one, abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 2 * y ≤ 1 + rexp y ∧ 1 ≤ rexp y + 2 * y
have refine : 1 ≤ rexp y + 2 * y
Tactic: refine ⟨le_trans two_mul_le_exp ((le_add_iff_nonneg_left (exp y)).mpr zero_le_one), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
⊢ LipschitzWith 1 ε.mulExpNegMulSq
have apply : ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1
Tactic: apply lipschitzWith_of_nnnorm_deriv_le differentiable_mulExpNegMulSq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹
have rw : (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹
Tactic: rw [mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one hε x, abs_mul, abs_of_pos (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹
have ha : 0 ≤ (√ε)⁻¹
Tactic: apply mul_le_of_le_one_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
ha : 0 ≤ (√ε)⁻¹
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹
have h : |mulExpNegMulSq 1 (√ε * x)| ≤ 1
Tactic: apply mul_le_of_le_one_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹
have apply : dist (ε.mulExpNegMulSq x) 0 + dist 0 (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹
Tactic: apply le_trans (dist_triangle (mulExpNegMulSq ε x) 0 (mulExpNegMulSq ε y))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) 0 + dist 0 (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹
have simp : |ε.mulExpNegMulSq x| + |ε.mulExpNegMulSq y| ≤ (√ε)⁻¹ + (√ε)⁻¹
Tactic: simp only [dist_zero_right, norm_eq_abs, dist_zero_left, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (hypothesis)
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
have h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ (↑1 : ℝ≥0∞) * edist x y
Tactic: have h := lipschitzWith_one_mulExpNegMulSq hε x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ (↑1 : ℝ≥0∞) * edist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
have rwa : ∀ (h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 1 * edist x y),
  dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
Tactic: rwa [ENNReal.coe_one, one_mul, ← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))] at h
Cleared hypotheses: h