-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem HasProd.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
    (ha : HasProd f a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) : HasProd g a

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
hu : ∀ b ≥ u, b ∈ (fun s => ∏ b ∈ s, f b) ⁻¹' s
⊢ ∀ x ∈ Set.Ici (image Sigma.fst u), ∏ b ∈ x, g b ∈ id s

Tactic:
intro bs hbs

Result:
case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
hu : ∀ b ≥ u, b ∈ (fun s => ∏ b ∈ s, f b) ⁻¹' s
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
⊢ ∏ b ∈ bs, g b ∈ id s

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
b : β
x✝ : b ∈ bs
⊢ 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✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (fun t => ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ bs, g b))

Tactic:
refine tendsto_finset_prod _ fun b _ ↦ ?_

Result:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
b : β
x✝ : b ∈ bs
⊢ Tendsto (fun t => ∏ s ∈ t.preimage (Sigma.mk b) ⋯, f ⟨b, s⟩) atTop (𝓝 (g b))

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
⊢ ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed ib → ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib

Tactic:
rintro s ⟨hs, hsc⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
⊢ HasProd g a

Tactic:
classical
refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
rintro s ⟨hs, hsc⟩
rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
use u.image Sigma.fst, trivial
intro bs hbs
simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
have : Tendsto (fun t : Finset (Σb, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
    (𝓝 <| ∏ b ∈ bs, 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))
refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (fun t => ∏ p ∈ filter (fun p => p.fst ∈ bs) t, f p) atTop (𝓝 (∏ b ∈ bs, g b))

Tactic:
simp only [← sigma_preimage_mk, prod_sigma]

Result:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (fun t => ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ bs, g b))

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ ∏ b ∈ bs, g b ∈ id s

Tactic:
have : Tendsto (fun t : Finset (Σb, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
    (𝓝 <| ∏ b ∈ bs, 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 right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this : Tendsto (fun t => ∏ p ∈ filter (fun p => p.fst ∈ bs) t, f p) atTop (𝓝 (∏ b ∈ bs, g b))
⊢ ∏ b ∈ bs, g b ∈ id s