awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
have 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
Tactic: refine ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ (∀ (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
have 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
Tactic: refine ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ ∃ (s : Finset β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
have 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
Tactic: obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 β), ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
have 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
Tactic: obtain ⟨s, hs⟩ := vanish o ho
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
have refine_1 : ∀ (t : Set β) (hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ (↑s : Set β)), ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
Tactic: refine ⟨s, fun t hts ↦ oe ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 β)
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
have pos : ∀ (ht : Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)),
  ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
Tactic: by_cases ht : Multipliable fun a : t ↦ f a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
have neg : ∀ (ht : ¬Multipliable.{u_1, u_2} (α := α) fun (a : (↑t : Type u_2)) ↦ f (↑a : β)),
  ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
Tactic: by_cases ht : Multipliable fun a : t ↦ f a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
have pos : ∀ (t' : Finset (↑t : Type u_2)), ∏ b ∈ t', (fun (a : (↑t : Type u_2)) ↦ f (↑a : β)) b ∈ o
Tactic: refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 ∈ t', (fun (a : (↑t : Type u_2)) ↦ f (↑a : β)) b ∈ o
have pos : ∏ x ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t', f x ∈ o
Tactic: rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t', f x ∈ o
have pos : ∀ ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t' → a ∉ s
Tactic: apply hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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)
⊢ ∀ ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t' → a ∉ s
have pos : ∀ ⦃a : β⦄, (∃ a_1 ∈ t', (Embedding.subtype fun (x : β) ↦ x ∈ t : (a : { x : β // x ∈ t }) → β) a_1 = a) → a ∉ s
Tactic: simp_rw [Finset.mem_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
have pos : ∀ (t' : Finset (↑t : Type u_2)), ∏ b ∈ t', (fun (a : (↑t : Type u_2)) ↦ f (↑a : β)) 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
have pos₁ : ∀ (t' : Finset (↑t : Type u_2)), ∏ x ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t', f x ∈ 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
have pos₂ : ∀ (t' : Finset (↑t : Type u_2)) ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun (x : β) ↦ x ∈ t) t' → a ∉ s
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ o
have pos₄ : ∀ (t' : Finset (↑t : Type u_2)) (b : { x : β // x ∈ t }),
  ((Embedding.subtype fun (x : β) ↦ x ∈ t : (a : { x : β // x ∈ t }) → β) b : β) ∉ s
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ ∃ (s : Finset β), ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
have 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
Tactic: obtain ⟨s, hs⟩ := vanish _ he
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
⊢ Multipliable f ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
have rw : (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: rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_prod_vanishing]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
rw :
  (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
⊢ Multipliable f ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
have rw₁ : (∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) ↔
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Tactic: rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_prod_vanishing]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
⊢ Multipliable f ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β), ∀ (t : Set β), Disjoint t (↑s : Set β) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
have rw : (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: rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
rw :
  (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
⊢ Multipliable f ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e →
        ∃ (s : Finset β), ∀ (t : Set β), Disjoint t (↑s : Set β) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
have rw₁ : (∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Set β), Disjoint t (↑s : Set β) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e) ↔
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e →
      ∃ (s : Finset β), ∀ (t : Set β), Disjoint t (↑s : Set β) → ∏' (b : (↑t : Type u_2)), f (↑b : β) ∈ e
Tactic: rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f g : β → α
inst_3 : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t with g b = f b, g b) (∏ b ∈ t, g b)
have refine : ∀ x ∈ t, x ∉ {b ∈ t | g b = f b} → g x = 1
Tactic: refine Finset.prod_subset (Finset.filter_subset _ _) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f g : β → α
inst_3 : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : b ∉ {b ∈ t | g b = f b}
⊢ g b = 1
have hb₁ : ¬g b = f b
Tactic: simp only [Finset.mem_filter, and_iff_right hbt] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f g : β → α
inst_3 : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t with g b = f b, g b) (∏ b ∈ t, g b)
have _ : ∀ x ∈ t, x ∉ {b ∈ t | g b = f b} → g x = 1
Tactic: {refine Finset.prod_subset (Finset.filter_subset _ _) ?_
            intro b hbt hb
            simp only [Finset.mem_filter, and_iff_right hbt] at hb
            exact (h b).resolve_right hb}
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f g : β → α
inst_3 : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
_ _₁ : ∀ (b : β) (hbt : b ∈ t) (hb : b ∉ {b ∈ t | g b = f b}), g b = 1
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t with g b = f b, g b) (∏ b ∈ t, g b)
have _₂ : ∀ (b : β) (hbt : b ∈ t) (hb : ¬g b = f b), g b = 1
Tactic: {refine Finset.prod_subset (Finset.filter_subset _ _) ?_
            intro b hbt hb
            simp only [Finset.mem_filter, and_iff_right hbt] at hb
            exact (h b).resolve_right hb}