-- Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean
theorem summable_iff_cauchySeq_finset_and_tsum_mem (f : β → α) :
    Summable f ↔ CauchySeq (fun s : Finset β ↦ ∑ b ∈ s, f b) ∧
      ∑' i, toCompl (f i) ∈ Set.range toCompl

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
constructor

Result:
case mpr.intro.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f)

case mpr.intro.right
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Proof state:
case mpr.intro.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ CauchySeq fun s => toCompl (∑ x ∈ s, f x)

Tactic:
exact h_cauchy.map (uniformContinuous_coe α)

Result:
no goals

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
a : α
ha : HasSum f a
⊢ (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
exact ⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩

Result:
no goals

Proof state:
case mpr.intro.right
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
exact h_tsum

Result:
no goals

Proof state:
case mpr.intro.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f)

Tactic:
apply summable_iff_cauchySeq_finset.mpr

Result:
case mpr.intro.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ CauchySeq fun s => ∑ b ∈ s, (⇑toCompl ∘ f) b

Proof state:
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
⊢ Summable f ↔ (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
⊢ Summable f → (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

case mpr
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
⊢ (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl → Summable f

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable f

Tactic:
apply (summable_iff_summable_compl_and_tsum_mem f).mpr

Result:
case mpr.intro
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Proof state:
case mpr.intro.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ CauchySeq fun s => ∑ b ∈ s, (⇑toCompl ∘ f) b

Tactic:
simp_rw [Function.comp_apply, ← map_sum]

Result:
case mpr.intro.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ CauchySeq fun s => toCompl (∑ x ∈ s, f x)

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
⊢ (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl → Summable f

Tactic:
rintro ⟨h_cauchy, h_tsum⟩

Result:
case mpr.intro
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s => ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable f

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
⊢ Summable f → (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
rintro ⟨a, ha⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f : β → α
a : α
ha : HasSum f a
⊢ (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl