awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
⊢ ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter

Tactic:
have h1 : ⋂ b ∈ (↑s ∩ L.support), {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem (Set.toFinite _)).mpr (fun b hb ↦ hb.2)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h :
  ∀ (t : Finset β)
    (ht : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s}) t)
    (ht' : (↑t : Set β) ⊆ L.support),
    Eq.{u_1 + 1} (α := α) (∏ b ∈ t, f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
⊢ ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)

Tactic:
filter_upwards [h1, L.eventually_le_support] with t ht ht'

Premises used: SummationFilter.HasSupport.eventually_le_support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s}) t
ht' : (↑t : Set β) ⊆ L.support
⊢ ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t

Tactic:
simp only [Set.mem_iInter] at ht

Premises used: Set.mem_iInter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht' : (↑t : Set β) ⊆ L.support
ht : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
h : ∀ a ∈ t, a ∉ ((↑s : Set β) ∩ L.support).toFinset → f a = 1
h₁ : ∀ a ∈ ((↑s : Set β) ∩ L.support).toFinset, a ∉ t → f a = 1
h₂ : ∀ a ∈ t, a ∈ ((↑s : Set β) ∩ L.support).toFinset → f a = f a
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t, f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)

Tactic:
apply Finset.prod_congr_of_eq_on_inter

Premises used: Finset.prod_congr_of_eq_on_inter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht' : (↑t : Set β) ⊆ L.support
ht : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
⊢ ∀ a ∈ t, a ∉ ((↑s : Set β) ∩ L.support).toFinset → f a = 1

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht' : (↑t : Set β) ⊆ L.support
ht : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
⊢ ∀ a ∈ ((↑s : Set β) ∩ L.support).toFinset, a ∉ t → f a = 1

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht' : (↑t : Set β) ⊆ L.support
ht : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
⊢ ∀ a ∈ t, a ∈ ((↑s : Set β) ∩ L.support).toFinset → f a = f a

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst_2 : L.LeAtTop
⊢ HasProd f (∏ b ∈ s, f b) L

Tactic:
((hasProd_subtype_iff_of_mulSupport_subset <| mulSupport_subset_iff'.2 hf).1 <| s.hasProd f)
    |>.mono_left L.le_atTop

Premises used: Iff.mpr, Function.mulSupport_subset_iff', HasProd, Set.Elem, SetLike.coe, Iff.mp, hasProd_subtype_iff_of_mulSupport_subset, Filter.Tendsto.mono_left, Finset.hasProd, SummationFilter.LeAtTop.le_atTop, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst_2 : L.HasSupport
⊢ Multipliable f L

Tactic:
(hasProd_prod_support_of_ne_finset_one (fun b _ hb ↦ hf b hb)).multipliable

Premises used: hasProd_prod_support_of_ne_finset_one, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst_2 : L.HasSupport
⊢ Multipliable f L

Tactic:
exact (hasProd_prod_support_of_ne_finset_one (fun b _ hb ↦ hf b hb)).multipliable

Premises used: hasProd_prod_support_of_ne_finset_one, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst_2 : L.HasSupport
⊢ Multipliable f L

Tactic:
classical
  exact (hasProd_prod_support_of_ne_finset_one (fun b _ hb ↦ hf b hb)).multipliable

Premises used: hasProd_prod_support_of_ne_finset_one, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
rw :
  HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
⊢ HasProd f (∏'[L] (b : β), f b) L

Tactic:
rw [tprod_def, dif_pos ha]

Premises used: dif_pos, tprod_def
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
pos :
  ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
    HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
pos₁ :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L), HasProd f 1 L
neg :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : ¬HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L),
    HasProd f (Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha) L
⊢ HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L

Tactic:
split_ifs with h h'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ HasProd f
    (∏
      b ∈
        ((↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ∩
            L.support).toFinset,
      f b)
    L

Tactic:
hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _

Premises used: hasProd_prod_support_of_ne_finset_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
h₁ :
  Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏
      b ∈
        ((↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ∩
            L.support).toFinset,
      f b)
pos : ∀ b ∈ L.support, b ∉ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support) → f b = 1
pos₁ : L.HasSupport
⊢ HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L

Tactic:
convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ (↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ⊆ L.support

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
h₁ :
  Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏ b ∈ (↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β).toFinset, f b)
⊢ Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏
      b ∈
        ((↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ∩
            L.support).toFinset,
      f b)

Tactic:
simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]

Premises used: Set.inter_eq_left, Iff.mpr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
h₁ :
  Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏ b ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)
⊢ Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏ b ∈ (↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β).toFinset, f b)

Tactic:
simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]

Premises used: Finset.toFinset_coe, Set.Finite.coe_toFinset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
h₁ :
  Eq.{u_1 + 1} (α := α)
    (∏ i ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support),
      L.support.mulIndicator (fun (b : β) ↦ f b) i)
    (∏ b ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)
h₂ :
  mulSupport.{u_2, u_1} (M := α) (L.support.mulIndicator fun (b : β) ↦ f b) ⊆
    (↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β)
⊢ Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏ b ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]

Premises used: finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ ∀ x ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support),
    L.support.mulIndicator (fun (b : β) ↦ f b) x = f x

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ Eq.{u_1 + 1} (α := α)
    (∏ i ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support),
      L.support.mulIndicator (fun (b : β) ↦ f b) i)
    (∏ b ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)

Tactic:
exact Finset.prod_congr rfl (by simp_all)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ mulSupport.{u_2, u_1} (M := α) (L.support.mulIndicator fun (b : β) ↦ f b) ⊆
    (↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ ∀ b ∈ L.support, b ∉ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support) → f b = 1

Tactic:
grind [Set.Finite.mem_toFinset, mem_mulSupport]

Premises used: Set.Finite.mem_toFinset, Function.mem_mulSupport
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ L.HasSupport

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ L.HasSupport

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite)
h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L
⊢ HasProd f 1 L

Tactic:
h'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite)
h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L
⊢ HasProd f 1 L

Tactic:
exact h'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite)
h' : ¬HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L
⊢ HasProd f (Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha) L

Tactic:
ha.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite)
h' : ¬HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L
⊢ HasProd f (Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha) L

Tactic:
exact ha.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
rw :
  HasProd f
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (b : β) ↦ f b)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) h
    else 1)
    L
rw₁ rw₂ rw₃ :
  HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
pos :
  ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
    HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
pos₁ :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L), HasProd f 1 L
neg :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : ¬HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L),
    HasProd f (Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha) L
pos₂ :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L), HasProd f 1 L
neg₁ neg₂ :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : ¬HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L),
    HasProd f (Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha) L
⊢ HasProd f (∏'[L] (b : β), f b) L

Tactic:
classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec

Premises used: Set.inter_eq_left, Iff.mpr, Exists.choose_spec, Set.Finite.mem_toFinset, Finset.toFinset_coe, Function.mem_mulSupport, dif_pos, Set.Finite.coe_toFinset, Finset.prod_congr, tprod_def, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
inst_2 : T2Space α
inst_3 : L.NeBot
a₁ a₂ : α
⊢ HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂

Tactic:
tendsto_nhds_unique

Premises used: HasProd, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
inst_2 : T2Space α
inst_3 : L.NeBot
a₁ a₂ : α
⊢ HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂

Tactic:
exact tendsto_nhds_unique

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
inst_2 : T2Space α
inst_3 : L.NeBot
a₁ a₂ : α
⊢ HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂

Tactic:
classical exact tendsto_nhds_unique

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : T2Space α
inst_3 : L.NeBot
ha : HasProd f a L
⊢ ∏'[L] (b : β), f b = a

Tactic:
(Multipliable.hasProd ⟨a, ha⟩).unique ha

Premises used: HasProd.unique, Multipliable.hasProd, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : T2Space α
inst_3 : L.NeBot
h : Multipliable f L
⊢ HasProd f a L ↔ ∏'[L] (b : β), f b = a

Tactic:
Iff.intro HasProd.tprod_eq fun eq ↦ eq ▸ h.hasProd

Premises used: Eq.rec, HasProd.tprod_eq, Multipliable.hasProd, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : T2Space α
L₁ L₂ : SummationFilter β
inst_3 : L₁.NeBot
h : L₁.filter ≤ L₂.filter
hf : Multipliable f L₂
⊢ Eq.{u_1 + 1} (α := α) (∏'[L₁] (b : β), f b) (∏'[L₂] (b : β), f b)

Tactic:
(hf.mono_filter h).hasProd_iff.mp (hf.hasProd.mono_left h)

Premises used: Multipliable.hasProd_iff, Multipliable.hasProd, Iff.mp, Filter.Tendsto.mono_left, Multipliable.mono_filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
inst_2 : T2Space α
inst_3 : L.NeBot
inst_4 : L.LeAtTop
hf : Multipliable f
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏' (b : β), f b)

Tactic:
tprod_eq_of_filter_le L.le_atTop hf

Premises used: tprod_eq_of_filter_le, SummationFilter.LeAtTop.le_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
inst : Monoid M
x : M
ab : M × M
⊢ ab ∈ mulFiber x ↔ ab.1 * ab.2 = x

Tactic:
simp [mulFiber]

Premises used: DiscreteConvolution.mulFiber
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
inst : Monoid M
⊢ Membership.mem (γ := Set (M × M)) (mulFiber 1) (1, 1)

Tactic:
simp [mulFiber]

Premises used: DiscreteConvolution.mulFiber
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : AddCommMonoid F
inst_5 : Module S E
inst_6 : Module S E'
inst_7 : Module S F
inst_8 : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E'
h : ∀ (x : M), (0 ⋆[L] f) x = 0 x
⊢ 0 ⋆[L] f = 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : AddCommMonoid F
inst_5 : Module S E
inst_6 : Module S E'
inst_7 : Module S F
inst_8 : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E'
x : M
⊢ (0 ⋆[L] f) x = 0 x

Tactic:
simp [convolution]

Premises used: DiscreteConvolution.convolution