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

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

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
⊢ ∃ 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)
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))

Tactic:
change
  Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g 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 => (fun t => ∏ s ∈ t, f ⟨b, s⟩) (t.preimage (Sigma.mk b) ⋯)) 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
⊢ ∀ s ∈ 𝓝 a, ∀ (a : Finset ((b : β) × γ b)), ∃ b, a ⊆ b ∧ ∏ i ∈ b, f i ∈ s

Tactic:
intro u hu s

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