-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem cauchySeq_finset_iff_prod_vanishing :
    (CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b) ↔
      ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e

Proof state:
case h.mk.intro
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
⊢ (∏ b ∈ (t₁, t₂).2, f b) / ∏ b ∈ (t₁, t₂).1, f b ∈ e

Tactic:
have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
  rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]

Result:
case h.mk.intro
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
this : (∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b
⊢ (∏ b ∈ (t₁, t₂).2, f b) / ∏ b ∈ (t₁, t₂).1, f b ∈ e

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ : Finset β
h : ∀ b ≥ (s₁, s₂), (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e
⊢ ∀ (t : Finset β), Disjoint t (s₁ ∪ s₂) → ∏ b ∈ t, f b ∈ e

Tactic:
intro t ht

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ : Finset β
h : ∀ b ≥ (s₁, s₂), (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e
t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
⊢ ∏ b ∈ t, f b ∈ e

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
⊢ (∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s) →
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
intro h e he

Result:
case mp
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h : ∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
⊢ ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e

Tactic:
use (s, s)

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
⊢ ∀ b ≥ (s, s), (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
⊢ (∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b

Tactic:
rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
⊢ (CauchySeq fun s => ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
simp only [CauchySeq, cauchy_map_iff, and_iff_right atTop_neBot, prod_atTop_atTop_eq,
  uniformity_eq_comap_nhds_one α, tendsto_comap_iff, Function.comp_def, atTop_neBot, true_and]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
⊢ Tendsto (fun x => (∏ b ∈ x.2, f b) / ∏ b ∈ x.1, f b) atTop (𝓝 1) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Proof state:
case h.mk.intro
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
this : (∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b
⊢ (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b ∈ e

Tactic:
exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h : ∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he

Result:
case mp.intro.mk
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ : Finset β
h : ∀ b ≥ (s₁, s₂), (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e