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 : β → α
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 β
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:
⟨s, fun t hts ↦ (t.tprod_subtype f).symm ▸ hs _ hts⟩

Premises used: Eq.rec, SetLike.coe, Exists.intro, Finset.tprod_subtype, 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 : 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 β
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:
exact ⟨s, fun t hts ↦ (t.tprod_subtype f).symm ▸ hs _ hts⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
rw₁ 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
⊢ Multipliable f ↔
    ∀ (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]

Premises used: multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_prod_vanishing
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
rw₁ 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
⊢ 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

Tactic:
rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing]

Premises used: multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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)

Tactic:
Finset.prod_subset (Finset.filter_subset _ _) ?_

Premises used: Finset.filter_subset, Finset.prod_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
refine : ∀ x ∈ t, x ∉ {b ∈ t | g b = f b} → g x = 1
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t with g b = f b, g b) (∏ b ∈ t, g b)

Tactic:
refine Finset.prod_subset (Finset.filter_subset _ _) ?_

Premises used: Finset.filter_subset, Finset.prod_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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 = f b

Tactic:
simp only [Finset.mem_filter, and_iff_right hbt] at hb

Premises used: and_iff_right, Finset.mem_filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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 : ¬g b = f b
⊢ g b = 1

Tactic:
(h b).resolve_right hb

Premises used: Or.resolve_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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 : ¬g b = f b
⊢ g b = 1

Tactic:
exact (h b).resolve_right hb

Premises used: Or.resolve_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
_₂ : ∀ (b : β) (hbt : b ∈ t) (hb : ¬g b = f b), g b = 1
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t with g b = f b, g b) (∏ b ∈ t, g b)

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}

Premises used: Finset.filter_subset, Finset.prod_subset, Finset.mem_filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
⊢ Multipliable g

Tactic:
exact multipliable_iff_vanishing.2 fun e he ↦
    let ⟨s, hs⟩ := multipliable_iff_vanishing.1 hf e he
    ⟨s, fun t ht ↦
      have eq : ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t, g b :=
        calc
          ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t with g b = f b, g b :=
            Finset.prod_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm
          _ = ∏ b ∈ t, g b := by
           {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}
      eq ▸ hs _ <| Finset.disjoint_of_subset_left (Finset.filter_subset _ _) ht⟩

Premises used: Iff.mpr, Trans.trans, Exists, Finset.prod_congr, And.right, multipliable_iff_vanishing, Exists.intro, Iff.mp, Finset.mem_filter, _private.0.Multipliable.multipliable_of_eq_one_or_self.match_1, Eq.symm, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
⊢ Multipliable g

Tactic:
classical
  exact multipliable_iff_vanishing.2 fun e he ↦
    let ⟨s, hs⟩ := multipliable_iff_vanishing.1 hf e he
    ⟨s, fun t ht ↦
      have eq : ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t, g b :=
        calc
          ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t with g b = f b, g b :=
            Finset.prod_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm
          _ = ∏ b ∈ t, g b := by
           {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}
      eq ▸ hs _ <| Finset.disjoint_of_subset_left (Finset.filter_subset _ _) ht⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
hf : Multipliable f
s : Set β
⊢ Multipliable (s.mulIndicator f)

Tactic:
hf.multipliable_of_eq_one_or_self <| Set.mulIndicator_eq_one_or_self _ _

Premises used: Set.mulIndicator_eq_one_or_self, Multipliable.multipliable_of_eq_one_or_self
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
i : γ → β
hf : Multipliable f
hi : Injective i
⊢ Multipliable (f ∘ i)

Tactic:
simpa only [Set.mulIndicator_range_comp] using
    (hi.multipliable_iff (fun x hx ↦ Set.mulIndicator_of_notMem hx _)).2
    (hf.mulIndicator (Set.range i))

Premises used: Iff.mpr, Set.mulIndicator_of_notMem, Multipliable.mulIndicator, Function.Injective.multipliable_iff, Set.range, Set.mulIndicator_range_comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
hf : Multipliable f
p : β → Prop
⊢ Multipliable (β := Subtype p) (f ∘ Subtype.val (p := p))

Tactic:
hf.comp_injective Subtype.coe_injective

Premises used: Subtype.coe_injective, Multipliable.comp_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
inst_3 : CompleteSpace α
s : Set β
⊢ ((Multipliable.{u_1, u_2} (α := α) fun (x : (↑s : Type u_2)) ↦ f (↑x : β)) ∧
      Multipliable.{u_1, u_2} (α := α) fun (x : (↑sᶜ : Type u_2)) ↦ f (↑x : β)) ↔
    Multipliable f

Tactic:
⟨and_imp.2 Multipliable.mul_compl, fun h ↦ ⟨h.subtype (· ∈ s), h.subtype (· ∈ sᶜ)⟩⟩

Premises used: Iff.mpr, Multipliable.subtype, Compl.compl, and_imp, Membership.mem, And.intro, Iff.intro, Multipliable.mul_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T2Space α
f : β → α
hf : Multipliable f
s : Set β
⊢ HMul.hMul (α := α) (∏' (x : (↑s : Type u_2)), f (↑x : β)) (∏' (x : (↑sᶜ : Type u_2)), f (↑x : β)) = ∏' (x : β), f x

Tactic:
((hf.subtype _).hasProd.mul_compl (hf.subtype _).hasProd).unique hf.hasProd

Premises used: Multipliable.subtype, HasProd.unique, Multipliable.hasProd, HasProd.mul_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
rw :
  HMul.hMul (α := α) (∏ x ∈ s, f x) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) =
    HMul.hMul (α := α) (∏' (x : (↑(↑s : Set β) : Type u_2)), f (↑x : β))
      (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β))
⊢ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) = ∏' (x : β), f x

Tactic:
rw [← hf.tprod_subtype_mul_tprod_subtype_compl s]

Premises used: SetLike.coe, Multipliable.tprod_subtype_mul_tprod_subtype_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
simp :
  Eq.{u_1 + 1} (α := α) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β))
⊢ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) =
    HMul.hMul (α := α) (∏' (x : (↑(↑s : Set β) : Type u_2)), f (↑x : β))
      (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β))

Tactic:
simp only [Finset.tprod_subtype', mul_right_inj]

Premises used: Finset.tprod_subtype', mul_right_inj
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ IsUniformGroup G

Tactic:
have : IsUniformGroup G := isUniformGroup_of_commGroup
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
this_1 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsUniformGroup G
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he

Premises used: Filter.Tendsto.cauchySeq, cauchySeq_finset_iff_prod_vanishing, Multipliable.hasProd, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
this_1 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsUniformGroup G
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he

Premises used: Filter.Tendsto.cauchySeq, cauchySeq_finset_iff_prod_vanishing, Multipliable.hasProd, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
letI letI₁ letI₂ : ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
letI₃ :
  let this := IsTopologicalGroup.rightUniformSpace G;
  ∀ (this : IsUniformGroup G), ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
classical
  letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
this_1 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsUniformGroup G
⊢ ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e

Tactic:
cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he

Premises used: Set.Mem, Filter.Tendsto.cauchySeq, cauchySeq_finset_iff_tprod_vanishing, Multipliable.hasProd, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
this_1 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsUniformGroup G
⊢ ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e

Tactic:
exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he

Premises used: Filter.Tendsto.cauchySeq, cauchySeq_finset_iff_tprod_vanishing, Multipliable.hasProd, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
letI letI₁ letI₂ : ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
letI₃ :
  let this := IsTopologicalGroup.rightUniformSpace G;
  ∀ (this : IsUniformGroup G),
    ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
⊢ ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e

Tactic:
classical
  letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
pos :
  ∀ (H : Multipliable f),
    Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
neg :
  ∀ (H : ¬Multipliable f),
    Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)

Tactic:
by_cases H : Multipliable f

Premises used: Multipliable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
pos :
  ∀ (s : Finset α) (hs : ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e),
    Membership.mem (γ := Filter G) (Filter.map (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop) e
⊢ Membership.mem (γ := Filter G) (Filter.map (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop) e

Tactic:
obtain ⟨s, hs⟩ := H.tprod_vanishing he

Premises used: Multipliable.tprod_vanishing
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset α
hs : ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
pos : ∃ (a : Finset α), ∀ b ≥ a, ∏' (a : { x : α // x ∉ b }), f (↑a : α) ∈ e
⊢ Membership.mem (γ := Filter G) (Filter.map (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop) e

Tactic:
simp only [Filter.mem_map, mem_atTop_sets, Set.mem_preimage]

Premises used: Filter.mem_atTop_sets, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset α
hs : ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
⊢ ∃ (a : Finset α), ∀ b ≥ a, ∏' (a : { x : α // x ∉ b }), f (↑a : α) ∈ e

Tactic:
⟨s, fun t hts ↦ hs tᶜ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩

Premises used: Iff.mpr, Compl.compl, Set.disjoint_left, SetLike.coe, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset α
hs : ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
⊢ ∃ (a : Finset α), ∀ b ≥ a, ∏' (a : { x : α // x ∉ b }), f (↑a : α) ∈ e

Tactic:
exact ⟨s, fun t hts ↦ hs tᶜ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)

Tactic:
tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm

Premises used: tendsto_const_nhds, tprod_eq_one_of_not_multipliable, Filter.Tendsto.congr, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
neg : ∀ (x : Finset α), ¬Multipliable.{u_4, u_1} (α := G) fun (a : { x_1 : α // x_1 ∉ x }) ↦ f (↑a : α)
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)

Tactic:
refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm

Premises used: tendsto_const_nhds, tprod_eq_one_of_not_multipliable, Filter.Tendsto.congr, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
x : Finset α
neg neg₁ neg₂ neg₃ : ¬Multipliable f
⊢ ¬Multipliable.{u_4, u_1} (α := G) fun (a : { x_1 : α // x_1 ∉ x }) ↦ f (↑a : α)

Tactic:
rwa [Finset.multipliable_compl_iff]

Premises used: Finset.multipliable_compl_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
pos :
  ∀ (H : Multipliable f),
    Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
neg neg₁ :
  ∀ (H : ¬Multipliable f),
    Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)

Tactic:
classical
  by_cases H : Multipliable f
  · intro e he
    obtain ⟨s, hs⟩ := H.tprod_vanishing he
    simp only [Filter.mem_map, mem_atTop_sets, Set.mem_preimage]
    exact ⟨s, fun t hts ↦ hs tᶜ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
  · refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
    rwa [Finset.multipliable_compl_iff]

Premises used: tendsto_const_nhds, Filter.mem_atTop_sets, Multipliable, tprod_eq_one_of_not_multipliable, Finset.multipliable_compl_iff, Filter.Tendsto.congr, Eq.symm, Filter.mem_map, Set.mem_preimage, SummationFilter.unconditional