awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
d : Set α
hd : Membership.mem (γ := Filter α) (𝓝 1) d
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
this : HDiv.hDiv (α := α) (∏ b ∈ t₂, f b) (∏ b ∈ t₁, f b) = HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)
h₁ : HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b) ∈ e
⊢ HDiv.hDiv (α := α) (∏ b ∈ (t₁, t₂).2, f b) (∏ b ∈ (t₁, t₂).1, f b) ∈ e

Tactic:
simp only [this]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
d : Set α
hd : Membership.mem (γ := Filter α) (𝓝 1) d
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
this : HDiv.hDiv (α := α) (∏ b ∈ t₂, f b) (∏ b ∈ t₁, f b) = HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)
⊢ HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b) ∈ e

Tactic:
hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

Premises used: Finset.sdiff_disjoint
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
d : Set α
hd : Membership.mem (γ := Filter α) (𝓝 1) d
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
this : HDiv.hDiv (α := α) (∏ b ∈ t₂, f b) (∏ b ∈ t₁, f b) = HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)
⊢ HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b) ∈ e

Tactic:
exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

Premises used: Finset.sdiff_disjoint
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
simp :
  Tendsto.{u_2, u_1} (β := α) (fun (x : Finset β × Finset β) ↦ HDiv.hDiv (α := α) (∏ b ∈ x.2, f b) (∏ b ∈ x.1, f b))
      atTop (𝓝 1) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
simp₁ :
  (∀ (s : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) s →
        ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
mp :
  (∀ (s : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) s →
        ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s) →
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
mpr mpr₁ :
  (∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) →
    ∀ (s : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) s →
        ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s
⊢ (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∏ b ∈ s, f b) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
classical
  simp only [CauchySeq, cauchy_map_iff, prod_atTop_atTop_eq,
    uniformity_eq_comap_nhds_one α, tendsto_comap_iff, Function.comp_def, atTop_neBot, true_and]
  rw [tendsto_atTop']
  constructor
  · intro h e he
    obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he
    use s₁ ∪ s₂
    intro t ht
    specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩
    simpa only [Finset.prod_union ht.symm, mul_div_cancel_left] using h
  · rintro h e he
    rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩
    rcases h d hd with ⟨s, h⟩
    use (s, s)
    rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
    have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
      rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]
    simp only [this]
    exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

Premises used: CauchySeq, cauchy_map_iff, Filter.atTop_neBot, Filter.tendsto_comap_iff, Function.comp_def, Filter.prod_atTop_atTop_eq, Filter.tendsto_atTop', uniformity_eq_comap_nhds_one, true_and, mul_div_cancel_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
simp_rw :
  (∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β),
          ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
⊢ (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∏ b ∈ s, f b) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β), ∀ (t : Set β), Disjoint t (↑s : Set β) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e

Tactic:
simp_rw [cauchySeq_finset_iff_prod_vanishing, Set.disjoint_left, disjoint_left]

Premises used: Set.disjoint_left, cauchySeq_finset_iff_prod_vanishing, Finset.disjoint_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
⊢ (∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β),
          ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e

Tactic:
⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
refine_1 :
  ∀
    (vanish :
      ∀ (e : Set α),
        Membership.mem (γ := Filter α) (𝓝 1) e →
          ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e)
    (e : Set α) (he : Membership.mem (γ := Filter α) (𝓝 1) e),
    ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
refine_2 :
  ∀
    (vanish :
      ∀ (e : Set α),
        Membership.mem (γ := Filter α) (𝓝 1) e →
          ∃ (s : Finset β),
            ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e)
    (e : Set α) (he : Membership.mem (γ := Filter α) (𝓝 1) e),
    ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
⊢ (∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β),
          ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e

Tactic:
refine ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
refine_1 :
  ∀ (o : Set α) (ho : Membership.mem (γ := Filter α) (𝓝 1) o) (o_closed : IsClosed[inst.toTopologicalSpace] o)
    (oe : o ⊆ e),
    ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
⊢ ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e

Tactic:
obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he

Premises used: exists_mem_nhds_isClosed_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
refine_1 :
  ∀ (s : Finset β) (hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o),
    ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
⊢ ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e

Tactic:
obtain ⟨s, hs⟩ := vanish o ho
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
⊢ ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e

Tactic:
⟨s, fun t hts ↦ oe ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
refine_1 : ∀ (t : Set β) (hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)), ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
⊢ ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e

Tactic:
refine ⟨s, fun t hts ↦ oe ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
pos :
  ∀ (ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)),
    ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
neg :
  ∀ (ht : ¬Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)),
    ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o

Tactic:
by_cases ht : Multipliable fun a : t ↦ f a

Premises used: Multipliable, Subtype.val, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o

Tactic:
o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
pos : ∀ (t' : Finset (↑t : Type u_2)), ∏ b ∈ t', (fun (a : (↑t : Type u_2)) ↦ f (↑a : β)) b ∈ o
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o

Tactic:
refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
t' : Finset (↑t : Type u_2)
x : { x : β // x ∈ t }
h : x ∈ t'
⊢ f (↑x : β) = f (↑x : β)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
t' : Finset (↑t : Type u_2)
pos : ∏ x ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t', f x ∈ o
⊢ ∏ b ∈ t', (fun (a : (↑t : Type u_2)) ↦ f (↑a : β)) b ∈ o

Tactic:
rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]

Premises used: Finset.prod_subtype_map_embedding
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
t' : Finset (↑t : Type u_2)
pos : ∀ ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t' → a ∉ s
⊢ ∏ x ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t', f x ∈ o

Tactic:
apply hs
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
t' : Finset (↑t : Type u_2)
pos : ∀ ⦃a : β⦄, (∃ a_1 ∈ t', (Embedding.subtype fun (x : β) ↦ x ∈ t : (a : { x : β // x ∈ t }) → β) a_1 = a) → a ∉ s
⊢ ∀ ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t' → a ∉ s

Tactic:
simp_rw [Finset.mem_map]

Premises used: Finset.mem_map
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
t' : Finset (↑t : Type u_2)
b : { x : β // x ∈ t }
⊢ ((Embedding.subtype fun (x : β) ↦ x ∈ t : (a : { x : β // x ∈ t }) → β) b : β) ∉ s

Tactic:
hts b.prop

Premises used: Subtype.prop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
t' : Finset (↑t : Type u_2)
b : { x : β // x ∈ t }
⊢ ((Embedding.subtype fun (x : β) ↦ x ∈ t : (a : { x : β // x ∈ t }) → β) b : β) ∉ s

Tactic:
exact hts b.prop

Premises used: Subtype.prop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
pos : ∀ (t' : Finset (↑t : Type u_2)), ∏ b ∈ t', (fun (a : (↑t : Type u_2)) ↦ f (↑a : β)) b ∈ o
pos₁ : ∀ (t' : Finset (↑t : Type u_2)), ∏ x ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t', f x ∈ o
pos₂ : ∀ (t' : Finset (↑t : Type u_2)) ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t' → a ∉ s
pos₃ :
  ∀ (t' : Finset (↑t : Type u_2)) ⦃a : β⦄,
    (∃ a_1 ∈ t', (Embedding.subtype fun (x : β) ↦ x ∈ t : (a : { x : β // x ∈ t }) → β) a_1 = a) → a ∉ s
pos₄ :
  ∀ (t' : Finset (↑t : Type u_2)) (b : { x : β // x ∈ t }),
    ((Embedding.subtype fun (x : β) ↦ x ∈ t : (a : { x : β // x ∈ t }) → β) b : β) ∉ s
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o

Tactic:
classical
      refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)
      rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]
      apply hs
      simp_rw [Finset.mem_map]
      rintro _ ⟨b, -, rfl⟩
      exact hts b.prop

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Multipliable.hasProd, Finset.prod_subtype_map_embedding, Finset.mem_map, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : ¬Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o

Tactic:
tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho

Premises used: Eq.rec, mem_of_mem_nhds, tprod_eq_one_of_not_multipliable, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
o : Set α
ho : Membership.mem (γ := Filter α) (𝓝 1) o
o_closed : IsClosed[inst.toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)
ht : ¬Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o

Tactic:
exact tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
vanish :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
refine_2 :
  ∀ (s : Finset β)
    (hs : ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e),
    ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
⊢ ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e

Tactic:
obtain ⟨s, hs⟩ := vanish _ he