-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem HasProd.of_sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
    (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hg : HasProd g a)
    (h : CauchySeq (fun (s : Finset (Σ b : β, γ b)) ↦ ∏ i ∈ s, f i)) :
    HasProd f a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
A : ∀ᶠ (t0 : Finset β) in atTop, ∏ i ∈ t0, g i ∈ v
⊢ ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ image Sigma.fst s ⊆ t0

Tactic:
exact (A.and (Ici_mem_atTop _)).exists

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
b : β
x✝ : b ∈ t0
⊢ Tendsto (fun t => (fun t => ∏ s ∈ t, f ⟨b, s⟩) (t.preimage (Sigma.mk b) ⋯)) atTop (𝓝 (g b))

Tactic:
exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
⊢ ClusterPt a (Filter.map (fun s => ∏ i ∈ s, f i) atTop)

Tactic:
simp only [← mapClusterPt_def, mapClusterPt_iff, frequently_atTop, ge_iff_le, le_eq_subset]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
⊢ ∀ s ∈ 𝓝 a, ∀ (a : Finset ((b : β) × γ b)), ∃ b, a ⊆ b ∧ ∏ i ∈ b, f i ∈ s

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
L : Tendsto (fun t => ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p) atTop (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p ∈ v
st : s ⊆ t
x : (b : β) × γ b
hx : x ∈ s
⊢ x ∈ filter (fun p => p.fst ∈ t0) t

Tactic:
simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
L : Tendsto (fun t => ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p) atTop (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p ∈ v
st : s ⊆ t
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
L : Tendsto (fun t => ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p) atTop (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p ∈ v
st : s ⊆ t
x : (b : β) × γ b
hx : x ∈ s
⊢ x ∈ filter (fun p => p.fst ∈ t0) t

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
⊢ Tendsto (fun t => ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ t0, g b))

Tactic:
refine tendsto_finset_prod _ fun b _ ↦ ?_

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
b : β
x✝ : b ∈ t0
⊢ Tendsto (fun t => ∏ s ∈ t.preimage (Sigma.mk b) ⋯, f ⟨b, s⟩) atTop (𝓝 (g b))

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
⊢ Tendsto (fun t => ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p) atTop (𝓝 (∏ b ∈ t0, g b))

Tactic:
simp only [← sigma_preimage_mk, prod_sigma]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
⊢ Tendsto (fun t => ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ t0, g b))

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
⊢ HasProd f a

Tactic:
apply le_nhds_of_cauchy_adhp h

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s => ∏ i ∈ s, f i
⊢ ClusterPt a (Filter.map (fun s => ∏ i ∈ s, f i) atTop)