-- 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:
case 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))
this : ∃ t, ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p ∈ v ∧ s ⊆ t
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
obtain ⟨t, tv, st⟩ := this

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
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Proof state:
case 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
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
have L : Tendsto (fun t : Finset (Σb, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop
    (𝓝 <| ∏ b ∈ t0, g b) := by
  simp only [← sigma_preimage_mk, prod_sigma]
  refine tendsto_finset_prod _ fun b _ ↦ ?_
  change
    Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
  exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))

Result:
case 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))
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Proof state:
case 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))
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
  ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists

Result:
case 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))
this : ∃ t, ∏ p ∈ filter (fun p => p.fst ∈ t0) t, f p ∈ v ∧ s ⊆ t
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

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)
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩

Result:
case 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
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

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:
classical
apply le_nhds_of_cauchy_adhp h
simp only [← mapClusterPt_def, mapClusterPt_iff, frequently_atTop, ge_iff_le, le_eq_subset]
intro u hu s
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
obtain ⟨t0, st0, ht0⟩ : ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ s.image Sigma.fst ⊆ t0 := by
  have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
  exact (A.and (Ici_mem_atTop _)).exists
have L : Tendsto (fun t : Finset (Σb, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop
    (𝓝 <| ∏ b ∈ t0, g b) := by
  simp only [← sigma_preimage_mk, prod_sigma]
  refine tendsto_finset_prod _ fun b _ ↦ ?_
  change
    Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
  exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
  ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists
obtain ⟨t, tv, st⟩ := this
refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)

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, ∏ i ∈ t0, g i ∈ v ∧ image Sigma.fst s ⊆ t0

Tactic:
have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)

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
A : ∀ᶠ (t0 : Finset β) in atTop, ∏ i ∈ t0, g i ∈ v
⊢ ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ image Sigma.fst s ⊆ t0