awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)

Tactic:
(this.mul_left _).tsum_eq.symm

Premises used: HasSum.mul_left, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)

Tactic:
exact (this.mul_left _).tsum_eq.symm

Premises used: HasSum.mul_left, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / HPow.hPow (α := ℝ) 2 n
⊢ CauchySeq f

Tactic:
cauchySeq_of_dist_le_of_summable _ hu₂ <| ⟨_, hasSum_geometric_two' C⟩

Premises used: cauchySeq_of_dist_le_of_summable, hasSum_geometric_two', Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
⊢ dist (f 0) a ≤ C

Tactic:
tsum_geometric_two' C ▸ dist_le_tsum_of_dist_le_of_tendsto₀ _ hu₂ (summable_geometric_two' C) ha

Premises used: Eq.rec, dist_le_tsum_of_dist_le_of_tendsto₀, tsum_geometric_two', summable_geometric_two'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 (n + m)

Tactic:
dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n

Premises used: dist_le_tsum_of_dist_le_of_tendsto, summable_geometric_two'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
h : C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 (n + m)
⊢ dist (f n) a ≤ C / HPow.hPow (α := ℝ) 2 n

Tactic:
convert! dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n

Premises used: dist_le_tsum_of_dist_le_of_tendsto, summable_geometric_two'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
h : C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n
⊢ C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 (n + m)

Tactic:
simp only [add_comm n, pow_add, ← div_div]

Premises used: pow_add, add_comm, div_div
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
h : ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n = C / HPow.hPow (α := ℝ) 2 n
⊢ C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n

Tactic:
symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
⊢ ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n = C / HPow.hPow (α := ℝ) 2 n

Tactic:
((hasSum_geometric_two' C).div_const _).tsum_eq

Premises used: HasSum.div_const, hasSum_geometric_two', HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
⊢ ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n = C / HPow.hPow (α := ℝ) 2 n

Tactic:
exact ((hasSum_geometric_two' C).div_const _).tsum_eq

Premises used: HasSum.div_const, hasSum_geometric_two', HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 ≤ 1 / m ^ f a

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
refine : ∀ (a : ℕ), 1 / m ^ f a ≤ (1 / m) ^ a
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ 1 / m ^ f i

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)))
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
rw : 1 / m ^ f a ≤ 1 / m ^ a
⊢ 1 / m ^ f a ≤ (1 / m) ^ a

Tactic:
rw [div_pow, one_pow]

Premises used: one_pow, div_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a

Tactic:
(one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a))

Premises used: Iff.mpr, LT.lt.le, one_div_le_one_div, pow_right_mono₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
refine_1 : 0 < m ^ f a
refine_2 : 0 < m ^ a
⊢ 1 / m ^ f a ≤ 1 / m ^ a

Tactic:
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a))

Premises used: Iff.mpr, LT.lt.le, one_div_le_one_div, pow_right_mono₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ f a

Tactic:
pow_pos (zero_lt_one.trans hm) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ f a

Tactic:
exact pow_pos (zero_lt_one.trans hm) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ a

Tactic:
pow_pos (zero_lt_one.trans hm) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ a

Tactic:
exact pow_pos (zero_lt_one.trans hm) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
⊢ HasSum f ε

Tactic:
have hf : HasSum f ε := hasSum_geometric_two' _
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ε
⊢ ∀ (n : ℕ), 0 < f n

Tactic:
have f0 : ∀ n, 0 < f n := fun n ↦ div_pos (half_pos hε) (pow_pos zero_lt_two _)
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
refine : ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
⊢ { ε' : ι → ℝ // (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum ε' c ∧ c ≤ ε }

Tactic:
refine ⟨f ∘ Encodable.encode, fun i ↦ f0 _, ?_⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
rcases : ∀ (c : ℝ) (hg : HasSum (f ∘ Encodable.encode) c), ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
⊢ ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε

Tactic:
rcases hf.summable.comp_injective (@Encodable.encode_injective ι _) with ⟨c, hg⟩

Premises used: Encodable.encode_injective, HasSum.summable, Summable.comp_injective
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ε

Tactic:
⟨c, hg, hasSum_le_inj _ (@Encodable.encode_injective ι _) ?_ ?_ hg hf⟩

Premises used: Encodable.encode_injective, And.intro, Exists.intro, hasSum_le_inj
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
refine_2 : ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)
⊢ ∃ (c : ℝ), HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε

Tactic:
refine ⟨c, hg, hasSum_le_inj _ (@Encodable.encode_injective ι _) ?_ ?_ hg hf⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
i : ℕ
refine_1 : i ∉ Set.range.{0, u_4 + 1} (ι := ι) Encodable.encode → 0 ≤ f i
⊢ i ∉ Set.range.{0, u_4 + 1} (ι := ι) Encodable.encode → 0 ≤ f i

Tactic:
_
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
i : ℕ
h : i ∉ Set.range.{0, u_4 + 1} (ι := ι) Encodable.encode
⊢ 0 ≤ f i

Tactic:
le_of_lt (f0 _)

Premises used: le_of_lt
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
i : ℕ
h : i ∉ Set.range.{0, u_4 + 1} (ι := ι) Encodable.encode
⊢ 0 ≤ f i

Tactic:
exact le_of_lt (f0 _)

Premises used: le_of_lt
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
n : ι
⊢ (f ∘ Encodable.encode) n ≤ f (Encodable.encode n)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
n : ι
⊢ (f ∘ Encodable.encode) n ≤ f (Encodable.encode n)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
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 ≤ ε

Tactic:
haveI := hs.toEncodable
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable (↑s : Type u_4)
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 ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (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ε⟩⟩

Premises used: Set.Elem, posSumOfEncodable
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ε

Tactic:
⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩

Premises used: Membership.mem, dite, Subtype.mk, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
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
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : (↑s : Type u_4)) ↦ ε' (↑i : ι)) c ∧ c ≤ ε

Tactic:
refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
neg : i ∉ s → LT.lt (α := ℝ) 0 1
⊢ LT.lt (α := ℝ) 0 (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ι
h : i ∈ s
⊢ 0 < f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h)

Tactic:
hf0 _
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ι
h : i ∉ s
⊢ LT.lt (α := ℝ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ι
h : i ∈ s
⊢ 0 < f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h)

Tactic:
exacts [hf0 _, zero_lt_one]

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ε
⊢ 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:
simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]

Premises used: Subtype.coe_prop, dif_pos, Subtype.coe_eta
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
refine_2 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
⊢ ∃ (ε' : ι → ℝ), (∀ (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]

Premises used: Subtype.coe_prop, dif_pos, zero_lt_one, Subtype.coe_eta
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ε

Tactic:
rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩

Premises used: Set.Countable.exists_pos_hasSum_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ε

Tactic:
⟨ε', hpos, fun t ht ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ε
refine : ∀ (t : Finset ι) (ht : (↑t : Set ι) ⊆ s), ∑ i ∈ t, ε' i ≤ ε
⊢ ∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Tactic:
refine ⟨ε', hpos, fun t ht ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
rw : ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' (↑x : ι) ≤ ε
⊢ ∑ i ∈ t, ε' i ≤ ε

Tactic:
rw [← sum_subtype_of_mem _ ht]

Premises used: Finset.sum_subtype_of_mem
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ι) ≤ ε

Tactic:
(sum_le_hasSum _ ?_ hε'c).trans hcε

Premises used: sum_le_hasSum, LE.le.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
refine : ∀ i ∉ Finset.subtype (Membership.mem s) t, 0 ≤ ε' (↑i : ι)
⊢ ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' (↑x : ι) ≤ ε

Tactic:
refine (sum_le_hasSum _ ?_ hε'c).trans hcε

Premises used: sum_le_hasSum, LE.le.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ∉ Finset.subtype (Membership.mem s) t, 0 ≤ ε' (↑i : ι)

Tactic:
fun _ _ ↦ (hpos _).le

Premises used: LT.lt.le, Subtype.val
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ∉ Finset.subtype (Membership.mem s) t, 0 ≤ ε' (↑i : ι)

Tactic:
exact fun _ _ ↦ (hpos _).le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ι) ≤ ε
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 : ι)
⊢ ∃ (ε' : ι → ℝ), (∀ (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

Premises used: Set.Countable.exists_pos_hasSum_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
intro : ∀ (val : Encodable ι), ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε

Tactic:
cases nonempty_encodable ι

Premises used: nonempty_encodable
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
val : Encodable ι
intro :
  ∀ (a : ℝ≥0) (a0 : 0 < a) (aε : a < ε), ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε

Tactic:
obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)

Premises used: Iff.mpr, exists_between, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
val : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
intro :
  ∀ (ε' : ι → ℝ) (hε' : ∀ (i : ι), 0 < ε' i) (c : ℝ) (hc : HasSum ε' c) (hcε : c ≤ (↑a : ℝ)),
    ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε

Tactic:
obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι

Premises used: posSumOfEncodable