-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem tendsto_tprod_compl_atTop_one (f : α → G) :
    Tendsto (fun s : Finset α ↦ ∏' a : { x // x ∉ s }, f a) atTop (𝓝 1)

Proof state:
case pos.intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ e ∈ Filter.map (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop

Tactic:
rw [Filter.mem_map, mem_atTop_sets]

Result:
case pos.intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ ∃ a, ∀ b ≥ a, b ∈ (fun s => ∏' (a : { x // x ∉ s }), f ↑a) ⁻¹' e

Proof state:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ e ∈ Filter.map (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop

Tactic:
obtain ⟨s, hs⟩ := H.tprod_vanishing he

Result:
case pos.intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ e ∈ Filter.map (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop

Proof state:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
⊢ Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop (𝓝 1)

Tactic:
intro e he

Result:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ e ∈ Filter.map (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop

Proof state:
case pos.intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ ∃ a, ∀ b ≥ a, b ∈ (fun s => ∏' (a : { x // x ∉ s }), f ↑a) ⁻¹' e

Tactic:
exact ⟨s, fun t hts ↦ hs _ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩

Result:
no goals

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
⊢ Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop (𝓝 1)

Tactic:
by_cases H : Multipliable f

Result:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
⊢ Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop (𝓝 1)

case neg
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
⊢ Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop (𝓝 1)

Proof state:
case neg
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
x✝ : Finset α
⊢ ¬Multipliable fun a => f ↑a

Tactic:
rwa [Finset.multipliable_compl_iff]

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
⊢ Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) atTop (𝓝 1)

Tactic:
refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm

Result:
case neg
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
x✝ : Finset α
⊢ ¬Multipliable fun a => f ↑a