awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
refine :
  ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
refine₁ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
refine₂ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b))
    (hu :
      ∀ b ≥ u,
        Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
right right₁ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b))
    (hu :
      ∀ b ≥ u,
        Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b)
    (bs : Finset β) (hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)), ∏ b ∈ bs, g b ∈ id s
⊢ HasProd g a
have right₂ : ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b)) (bs : Finset β)
  (hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u))
  (hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s), ∏ b ∈ bs, g b ∈ id s
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_finsetProd _ 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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
refine :
  ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
refine₁ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
refine₂ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b))
    (hu :
      ∀ b ≥ u,
        Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
right right₁ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b))
    (hu :
      ∀ b ≥ u,
        Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b)
    (bs : Finset β) (hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)), ∏ b ∈ bs, g b ∈ id s
right₂ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b)) (bs : Finset β)
    (hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u))
    (hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s), ∏ b ∈ bs, g b ∈ id s
⊢ HasProd g a
have right₃ : ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b)) (bs : Finset β)
  (hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u))
  (hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s)
  (this :
    Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
      (𝓝 (∏ b ∈ bs, g b))),
  ∏ b ∈ bs, g b ∈ id s
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_finsetProd _ 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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable.{u_1, u_2} (α := α) fun (b : β) ↦ f b c
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ) (b : β), f b c) (∏' (b : β) (c : γ), f b c)
have rw : Eq.{u_1 + 1} (α := α) (∏' (p : γ × β), uncurry (fun (b : γ) (c : β) ↦ f c b) p)
  (∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β : (a : γ × β) → β × γ) c))
Tactic: rw [← h.tprod_prod_uncurry h₁, ← h.prod_symm.tprod_prod_uncurry h₂,
    ← (Equiv.prodComm γ β).tprod_eq (uncurry f)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
⊢ HasProd f a
have apply : ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
Tactic: apply le_nhds_of_cauchy_adhp h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
⊢ ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
have simp : ∀ s ∈ 𝓝 a, ∀ (a : Finset ((b : β) × γ b)), ∃ (b : Finset ((b : β) × γ b)), a ⊆ b ∧ ∏ i ∈ b, f i ∈ s
Tactic: simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop, ge_iff_le,
    le_eq_subset]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
have rcases : ∀ (v : Set α) (vu : v ⊆ u) (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v),
  ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Tactic: rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
⊢ ∃ (t0 : Finset β), ∏ i ∈ t0, g i ∈ v ∧ image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
have A : ∀ᶠ (t0 : Finset β) in atTop, ∏ i ∈ t0, g i ∈ v
Tactic: have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
have obtain : ∀ (t0 : Finset β) (st0 : ∏ i ∈ t0, g i ∈ v) (ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0),
  ∃ (b : Finset ((b : β) × γ 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
⊢ Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
have simp : Tendsto (β := α)
  (fun (t : Finset ((b : β) × γ b)) ↦
    ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) sorry, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
  atTop (𝓝 (∏ b ∈ t0, g b))
Tactic: simp only [← sigma_preimage_mk, prod_sigma]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
⊢ Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ t0, g b))
have refine : ∀ b ∈ t0,
  Tendsto
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) b) sorry, f (Sigma.mk (β := fun (a : β) ↦ γ a) b s))
    atTop (𝓝 (g b))
Tactic: refine tendsto_finsetProd _ fun b _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
have L : Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
  (𝓝 (∏ b ∈ t0, g b))
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_finsetProd _ 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))
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
have this : ∃ (t : Finset ((b : β) × γ b)), ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v ∧ s ⊆ t
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
this : ∃ (t : Finset ((b : β) × γ b)), ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v ∧ s ⊆ t
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
have obtain : ∀ (t : Finset ((b : β) × γ b)) (tv : ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v) (st : s ⊆ t),
  ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Tactic: obtain ⟨t, tv, st⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v
st : s ⊆ t
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
have refine : ∀ (x : (b : β) × γ b) (hx : x ∈ s), x ∈ {p ∈ t | p.fst (β := fun (b : β) ↦ γ b) ∈ t0}
Tactic: refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
⊢ HasProd f a
have apply : ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
Tactic: classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, 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_finsetProd _ 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
apply : ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
⊢ HasProd f a
have apply₁ : ∀ s ∈ 𝓝 a, ∀ (a : Finset ((b : β) × γ b)), ∃ (b : Finset ((b : β) × γ b)), a ⊆ b ∧ ∏ i ∈ b, f i ∈ s
Tactic: classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, 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_finsetProd _ 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
apply : ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
apply₁ apply₂ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
⊢ HasProd f a
have apply₃ : ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)) (v : Set α) (vu : v ⊆ u)
  (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Tactic: classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, 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_finsetProd _ 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
apply : ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
apply₁ apply₂ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
apply₃ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)) (v : Set α) (vu : v ⊆ u)
    (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v),
    ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
⊢ HasProd f a
have apply₄ : ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)) (v : Set α) (vu : v ⊆ u)
  (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v) (t0 : Finset β) (st0 : ∏ i ∈ t0, g i ∈ v)
  (ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Tactic: classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, 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_finsetProd _ 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)