-- 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 mpr
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
f : β → α
⊢ (∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) →
    ∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s

Tactic:
rintro h e he

Result:
case mpr
α : 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
⊢ ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.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₂ t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
h : (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).2, f b) / ∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).1, f b ∈ e
⊢ ∏ b ∈ t, f b ∈ e

Tactic:
simpa only [Finset.prod_union ht.symm, mul_div_cancel_left] using h

Result:
no goals

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₁, t₂).2, f b) / ∏ b ∈ (t₁, t₂).1, f b ∈ e

Tactic:
simp only [this]

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₂ \ s, f b) / ∏ b ∈ t₁ \ s, 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 β
ht : Disjoint t (s₁ ∪ s₂)
⊢ ∏ b ∈ t, f b ∈ e

Tactic:
specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩

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₂ t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
h : (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).2, f b) / ∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).1, f b ∈ e
⊢ ∏ b ∈ t, f b ∈ e

Proof state:
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

Tactic:
use s₁ ∪ s₂

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 β), Disjoint t (s₁ ∪ s₂) → ∏ b ∈ t, f b ∈ e

Proof state:
case mpr.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
⊢ ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e

Tactic:
rcases h d hd with ⟨s, h⟩

Result:
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

Proof state:
case mpr
α : 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
⊢ ∃ a, ∀ b ≥ a, (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e

Tactic:
rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩

Result:
case mpr.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
⊢ ∃ a, ∀ b ≥ a, (∏ 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 : β → α
⊢ 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

Tactic:
rw [tendsto_atTop']

Result:
α : 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

Proof state:
α : 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:
constructor

Result:
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

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

Proof state:
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

Tactic:
rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩

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
⊢ (∏ b ∈ (t₁, t₂).2, f b) / ∏ b ∈ (t₁, t₂).1, f b ∈ e