awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / HPow.hPow (α := ℝ) 2 n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n
have h : ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n = C / HPow.hPow (α := ℝ) 2 n
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ 1 / m ^ f i
have refine : ∀ (a : ℕ), 1 / m ^ f a ≤ (1 / m) ^ a
Tactic: refine .of_nonneg_of_le (fun a ↦ by positivity) (fun a ↦ ?_)
      (summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le))
        ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a
have rw : 1 / m ^ f a ≤ 1 / m ^ a
Tactic: rw [div_pow, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a
have refine_1 : 0 < m ^ f a
Tactic: refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a))
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
refine_1 : 0 < m ^ f a
⊢ 1 / m ^ f a ≤ 1 / m ^ a
have refine_2 : 0 < m ^ a
Tactic: refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a))
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type u_4
inst : Encodable ι
f : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ε / 2 / HPow.hPow (α := ℝ) 2 n
⊢ { ε' : ι → ℝ // (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum ε' c ∧ c ≤ ε }
have hf : HasSum f ε
Tactic: have hf : HasSum f ε := hasSum_geometric_two' _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type u_4
inst : Encodable ι
f : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ε / 2 / HPow.hPow (α := ℝ) 2 n
hf : HasSum f ε
⊢ { ε' : ι → ℝ // (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum ε' c ∧ c ≤ ε }
have f0 : ∀ (n : ℕ), 0 < f n
Tactic: have f0 : ∀ n, 0 < f n := fun n ↦ div_pos (half_pos hε) (pow_pos zero_lt_two _)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type u_4
inst : Encodable ι
f : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ε / 2 / HPow.hPow (α := ℝ) 2 n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
⊢ { ε' : ι → ℝ // (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum ε' c ∧ c ≤ ε }
have refine : ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
Tactic: refine ⟨f ∘ Encodable.encode, fun i ↦ f0 _, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type u_4
inst : Encodable ι
f : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ε / 2 / HPow.hPow (α := ℝ) 2 n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
⊢ ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
have rcases : ∀ (c : ℝ) (hg : HasSum (f ∘ Encodable.encode) c), ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
Tactic: rcases hf.summable.comp_injective (@Encodable.encode_injective ι _) with ⟨c, hg⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type u_4
inst : Encodable ι
f : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ε / 2 / HPow.hPow (α := ℝ) 2 n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
have refine_1 : ∀ c ∉ Set.range.{0, u_4 + 1} (ι := ι) Encodable.encode, 0 ≤ f c
Tactic: refine ⟨c, hg, hasSum_le_inj _ (@Encodable.encode_injective ι _) ?_ ?_ hg hf⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type u_4
inst : Encodable ι
f : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ε / 2 / HPow.hPow (α := ℝ) 2 n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
refine_1 : ∀ c ∉ Set.range.{0, u_4 + 1} (ι := ι) Encodable.encode, 0 ≤ f c
⊢ ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
have refine_2 : ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)
Tactic: refine ⟨c, hg, hasSum_le_inj _ (@Encodable.encode_injective ι _) ?_ ?_ hg hf⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have haveI : ∀ (this : Encodable (↑s : Type u_4)),
  ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
Tactic: haveI := hs.toEncodable
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable (↑s : Type u_4)
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have rcases : ∀ (f : (↑s : Type u_4) → ℝ) (hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i) (c : ℝ) (hfc : HasSum f c) (hcε : c ≤ ε),
  ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
Tactic: rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable (↑s : Type u_4)
f : (↑s : Type u_4) → ℝ
hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have refine_1 : ∀ (i : ι),
  LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1 : ℝ)) i)
Tactic: refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable (↑s : Type u_4)
f : (↑s : Type u_4) → ℝ
hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
refine_1 :
  ∀ (i : ι),
    LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1 : ℝ)) i)
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have refine_2 : HasSum
  (fun (i : (↑s : Type u_4)) ↦
    (fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1 : ℝ)) (↑i : ι))
  c
Tactic: refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable (↑s : Type u_4)
f : (↑s : Type u_4) → ℝ
hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ LT.lt (α := ℝ) 0 (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1)
have pos : ∀ (h : i ∈ s), 0 < f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable (↑s : Type u_4)
f : (↑s : Type u_4) → ℝ
hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
pos : ∀ (h : i ∈ s), 0 < f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h)
⊢ LT.lt (α := ℝ) 0 (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1)
have neg : i ∉ s → LT.lt (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have haveI : ∀ (this : Encodable (↑s : Type u_4)),
  ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
Tactic: classical
  haveI := hs.toEncodable
  rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
  refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
  · conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]
  · simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
haveI haveI₁ haveI₂ :
  ∀ (this : Encodable (↑s : Type u_4)),
    ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have haveI₃ : ∀ (this : Encodable (↑s : Type u_4)) (f : (↑s : Type u_4) → ℝ) (hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i) (c : ℝ)
  (hfc : HasSum f c) (hcε : c ≤ ε),
  ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
Tactic: classical
  haveI := hs.toEncodable
  rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
  refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
  · conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]
  · simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
haveI haveI₁ haveI₂ :
  ∀ (this : Encodable (↑s : Type u_4)),
    ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
haveI₃ :
  ∀ (this : Encodable (↑s : Type u_4)) (f : (↑s : Type u_4) → ℝ) (hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i) (c : ℝ)
    (hfc : HasSum f c) (hcε : c ≤ ε),
    ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have refine_1 : ∀ (this : Encodable (↑s : Type u_4)) (f : (↑s : Type u_4) → ℝ) (hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i) (c : ℝ)
  (hfc : HasSum f c) (hcε : c ≤ ε) (i : ι),
  LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1 : ℝ)) i)
Tactic: classical
  haveI := hs.toEncodable
  rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
  refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
  · conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]
  · simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
haveI haveI₁ haveI₂ :
  ∀ (this : Encodable (↑s : Type u_4)),
    ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
haveI₃ :
  ∀ (this : Encodable (↑s : Type u_4)) (f : (↑s : Type u_4) → ℝ) (hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i) (c : ℝ)
    (hfc : HasSum f c) (hcε : c ≤ ε),
    ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
refine_1 :
  ∀ (this : Encodable (↑s : Type u_4)) (f : (↑s : Type u_4) → ℝ) (hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i) (c : ℝ)
    (hfc : HasSum f c) (hcε : c ≤ ε) (i : ι),
    LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1 : ℝ)) i)
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε
have refine_2 : ∀ (this : Encodable (↑s : Type u_4)) (f : (↑s : Type u_4) → ℝ) (hf0 : ∀ (i : (↑s : Type u_4)), 0 < f i) (c : ℝ)
  (hfc : HasSum f c) (hcε : c ≤ ε),
  HasSum
    (fun (i : (↑s : Type u_4)) ↦
      (fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1 : ℝ)) (↑i : ι))
    c
Tactic: classical
  haveI := hs.toEncodable
  rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
  refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
  · conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]
  · simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
have rcases : ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
  (hcε : c ≤ ε), ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
Tactic: rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c
hcε : c ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
have refine : ∀ (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∑ i ∈ t, ε' i ≤ ε
Tactic: refine ⟨ε', hpos, fun t ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c
hcε : c ≤ ε
t : Finset ι
ht : (↑t : Set ι) ⊆ s
⊢ ∑ i ∈ t, ε' i ≤ ε
have rw : ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' (↑x : ι) ≤ ε
Tactic: rw [← sum_subtype_of_mem _ ht]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c
hcε : c ≤ ε
t : Finset ι
ht : (↑t : Set ι) ⊆ s
⊢ ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' (↑x : ι) ≤ ε
have refine : ∀ i ∉ Finset.subtype (Membership.mem s) t, 0 ≤ ε' (↑i : ι)
Tactic: refine (sum_le_hasSum _ ?_ hε'c).trans hcε
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
have rcases : ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
  (hcε : c ≤ ε), ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
Tactic: classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
rcases :
  ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
    (hcε : c ≤ ε), ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
have rcases₁ : ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
  (hcε : c ≤ ε) (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∑ i ∈ t, ε' i ≤ ε
Tactic: classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
rcases :
  ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
    (hcε : c ≤ ε), ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
rcases₁ :
  ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
    (hcε : c ≤ ε) (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∑ i ∈ t, ε' i ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
have rcases₂ : ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
  (hcε : c ≤ ε) (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' (↑x : ι) ≤ ε
Tactic: classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
rcases :
  ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
    (hcε : c ≤ ε), ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
rcases₁ :
  ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
    (hcε : c ≤ ε) (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∑ i ∈ t, ε' i ≤ ε
rcases₂ :
  ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
    (hcε : c ≤ ε) (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' (↑x : ι) ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε
have rcases₃ : ∀ (ε' : ι → ℝ) (hpos : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hε'c : HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c)
  (hcε : c ≤ ε) (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∀ i ∉ Finset.subtype (Membership.mem s) t, 0 ≤ ε' (↑i : ι)
Tactic: classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
have intro : ∀ (val : Encodable ι), ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
Tactic: cases nonempty_encodable ι
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
val : Encodable ι
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
have intro : ∀ (a : ℝ≥0) (a0 : 0 < a) (aε : a < ε), ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
Tactic: obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
val : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
have intro : ∀ (ε' : ι → ℝ) (hε' : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hc : HasSum ε' c) (hcε : c ≤ (↑a : ℝ)),
  ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
Tactic: obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
have rcases : ∀ (r : ℝ≥0∞) (h0r : 0 < r) (hrε : r < ε), ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
Tactic: rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
have rcases : ∀ (x : ℝ≥0),
  (↑x : ℝ≥0∞) < ε →
    ∀ (h0r : 0 < (↑x : ℝ≥0∞)) (hrε : (↑x : ℝ≥0∞) < ε),
      ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
Tactic: rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩
Cleared hypotheses: r, h0r, hrε
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
x : ℝ≥0
right : (↑x : ℝ≥0∞) < ε
h0r : 0 < (↑x : ℝ≥0∞)
hrε : (↑x : ℝ≥0∞) < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
have rcases : ∀ (ε' : ι → ℝ≥0) (hp : ∀ (i : ι), 0 < ε' i) (c : ℝ≥0) (hc : HasSum ε' c) (hcr : c < x),
  ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
Tactic: rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w : ι → ℝ≥0∞
hw : ∀ (i : ι), w i ≠ ∞
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * (↑(δ i) : ℝ≥0∞) < ε
have lift : ∀ (w : (i : ι) → ℝ≥0),
  ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε
Tactic: lift w to ι → ℝ≥0 using hw
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w : (i : ι) → ℝ≥0
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε
have rcases : ∀ (δ' : ι → ℝ≥0) (Hpos : ∀ (i : ι), 0 < δ' i) (Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε),
  ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε
Tactic: rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε
have this : ∀ (i : ι), 0 < max 1 (w i)
Tactic: have : ∀ i, 0 < max 1 (w i) := fun i ↦ zero_lt_one.trans_le (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε
have refine : ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) < ε
Tactic: refine ⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) < ε
have refine : ∀ (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞)
Tactic: refine lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞)
have rw : (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * ((↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞)) ≤ (↑(δ' i) : ℝ≥0∞)
Tactic: rw [coe_div (this i).ne']