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 β
hL : ¬L.NeBot
f : β → α
a : α
⊢ L.filter = ⊥

Tactic:
have : L.filter = ⊥ := by contrapose! hL; exact ⟨hL⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
rw : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) ⊥ (𝓝 a)
⊢ HasProd f a L

Tactic:
rw [HasProd, this]

Premises used: HasProd, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
⊢ Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) ⊥ (𝓝 a)

Tactic:
tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
⊢ Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) ⊥ (𝓝 a)

Tactic:
exact tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
⊢ Multipliable f L

Tactic:
⟨1, hasProd_bot hL ..⟩

Premises used: Multipliable, hasProd_bot, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
simp :
  (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) ⋯) =
    ∏ᶠ (b : β), f b
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ᶠ (b : β), f b)

Tactic:
simp only [tprod_def, dif_pos (multipliable_bot hL f)]

Premises used: dif_pos, tprod_def, multipliable_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
⊢ L.LeAtTop

Tactic:
haveI : L.LeAtTop := L.leAtTop_of_not_NeBot hL
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
rw :
  (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (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) ⋯) =
    ∏ᶠ (b : β), f b
⊢ (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) ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
rw [L.support_eq_univ, Set.inter_univ, Set.mulIndicator_univ]

Premises used: SummationFilter.support_eq_univ, Set.inter_univ, Set.mulIndicator_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
pos :
  ∀ (hf : (mulSupport f).Finite),
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (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) ⋯) =
      ∏ᶠ (b : β), f b
neg :
  ∀ (hf : ¬(mulSupport f).Finite),
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (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) ⋯) =
      ∏ᶠ (b : β), f b
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (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) ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
by_cases hf : (mulSupport f).Finite

Premises used: Set.Finite, Function.mulSupport
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
pos : L.HasSupport ∧ True
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (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) ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
rw [eq_true_intro hf, if_pos]

Premises used: eq_true_intro, if_pos
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
pos : L.HasSupport
⊢ L.HasSupport ∧ True

Tactic:
simp only [and_true]

Premises used: and_true
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ L.HasSupport

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
tauto : L.HasSupport → Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) → False
⊢ ¬(L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b))

Tactic:
tauto
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
neg :
  (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) ⋯) =
    ∏ᶠ (b : β), f b
neg₁ : Eq.{u_1 + 1} (α := α) 1 (∏ᶠ (b : β), f b)
neg₂ : Eq.{u_1 + 1} (α := α) 1 1
neg₃ : (mulSupport f).Infinite
neg₄ : Eq.{u_1 + 1} (α := α) 1 1
neg₅ neg₆ neg₇ : (mulSupport f).Infinite
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (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) ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]

Premises used: if_pos, hasProd_bot, finprod_of_infinite_mulSupport, if_neg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
h : HasProd f a L
⊢ Multipliable f L

Tactic:
⟨a, h⟩

Premises used: Multipliable, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
h : ¬Multipliable f L
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) 1

Tactic:
simp [tprod_def, h]

Premises used: tprod_def
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter γ
g : γ → β
hg : Injective g
⊢ HasProd f a (L.map { toFun := g, inj' := hg }) ↔ HasProd (f ∘ g) a L

Tactic:
simp [HasProd, Function.comp_def]

Premises used: HasProd, Function.comp_def, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
simp :
  Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]

Premises used: Filter.tendsto_map'_iff, HasProd, SummationFilter.comap_filter, Function.comp_def, Function.Embedding.coeFn_mk, Function.comp_apply, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
tendsto_congr' ?_

Premises used: Filter.tendsto_congr'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
refine :
  EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) fun (s : Finset β) ↦
    ∏ b ∈ s, f b
⊢ Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
refine tendsto_congr' ?_

Premises used: Filter.tendsto_congr'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
h :
  ∀ (s : Finset β) (hs : (↑s : Set β) ⊆ L.support), Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g ⋯, f (g x)) (∏ b ∈ s, f b)
⊢ EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) fun (s : Finset β) ↦
    ∏ b ∈ s, f b

Tactic:
filter_upwards [L.eventually_le_support] with s hs

Premises used: SummationFilter.HasSupport.eventually_le_support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
s : Finset β
hs : (↑s : Set β) ⊆ L.support
h : ∀ x ∈ s, x ∉ Set.range g → f x = 1
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g ⋯, f (g x)) (∏ b ∈ s, f b)

Tactic:
rw [s.prod_preimage]

Premises used: Finset.prod_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
s : Finset β
hs : (↑s : Set β) ⊆ L.support
⊢ ∀ x ∈ s, x ∉ Set.range g → f x = 1

Tactic:
fun x h h' ↦ hf x (hs h) h'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
s : Finset β
hs : (↑s : Set β) ⊆ L.support
⊢ ∀ x ∈ s, x ∉ Set.range g → f x = 1

Tactic:
exact fun x h h' ↦ hf x (hs h) h'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
simp :
  Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]

Premises used: Filter.tendsto_map'_iff, HasProd, SummationFilter.comap_filter, Function.comp_def, Function.Embedding.coeFn_mk, Function.comp_apply, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
tendsto_congr fun s ↦ ?_

Premises used: Filter.tendsto_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
refine : ∀ (s : Finset β), Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g ⋯, f (g x)) (∏ b ∈ s, f b)
⊢ Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
refine tendsto_congr fun s ↦ ?_

Premises used: Filter.tendsto_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
s : Finset β
hg₁ : ∀ x ∈ s, x ∉ Set.range g → f x = 1
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g ⋯, f (g x)) (∏ b ∈ s, f b)

Tactic:
rw [s.prod_preimage]

Premises used: Finset.prod_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
s : Finset β
⊢ ∀ x ∈ s, x ∉ Set.range g → f x = 1

Tactic:
fun x _ h ↦ hf x h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
s : Finset β
⊢ ∀ x ∈ s, x ∉ Set.range g → f x = 1

Tactic:
exact fun x _ h ↦ hf x h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
rw : HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a ((unconditional β).comap { toFun := g, inj' := hg })
rw₁ rw₂ : HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a
⊢ HasProd (f ∘ g) a ↔ HasProd f a

Tactic:
rw [← hg.hasProd_comap_iff hf, SummationFilter.comap_unconditional]

Premises used: Function.Injective.hasProd_comap_iff, SummationFilter.comap_unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ ∀ x ∉ Set.range fun (a : { x : β // x ∈ s }) ↦ (↑a : β), f x = 1

Tactic:
simpa using mulSupport_subset_iff'.1 hf

Premises used: Function.mulSupport_subset_iff', Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔ HasProd f a

Tactic:
simpa using hasProd_subtype_comap_iff_of_mulSupport_subset hf (L := unconditional _)

Premises used: hasProd_subtype_comap_iff_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h : ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ L.support.toFinset, f b)
⊢ HasProd f (∏ b ∈ L.support.toFinset, f b) L

Tactic:
apply tendsto_nhds_of_eventually_eq

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
tauto tauto₁ tauto₂ : ∀ i ∈ L.support, {s : Finset β | i ∈ s} ∈ L.filter
⊢ ∀ i ∈ L.support, {s : Finset β | i ∈ s} ∈ L.filter

Tactic:
tauto
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
⊢ ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter

Tactic:
have h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem L.support.toFinite).mpr (by tauto)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
⊢ ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter

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

Tactic:
filter_upwards [h1, h2] with s hs hs'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
s : Finset β
hs : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.support, {s : Finset β | b ∈ s}) s
hs' : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s}) s
h : s = L.support.toFinset
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ s, f b) (∏ b ∈ L.support.toFinset, f b)

Tactic:
congr 1
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
s : Finset β
hs : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.support, {s : Finset β | b ∈ s}) s
hs' : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s}) s
⊢ ∀ (i : β) (i_1 : i ∈ L.support), i ∈ s

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq, Set.mem_compl_iff] at hs hs'

Premises used: Set.mem_setOf_eq, Set.mem_iInter, Set.mem_compl_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
s : Finset β
hs : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.support, {s : Finset β | b ∈ s}) s
hs' : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s}) s
hs₁ : ∀ (i : β) (i_1 : i ∈ L.support), i ∈ s
⊢ ∀ (i : β) (i_1 : i ∉ L.support), i ∉ s

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq, Set.mem_compl_iff] at hs hs'

Premises used: Set.mem_setOf_eq, Set.mem_iInter, Set.mem_compl_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
s : Finset β
hs : ∀ (i : β) (i_1 : i ∈ L.support), i ∈ s
hs' : ∀ (i : β) (i_1 : i ∉ L.support), i ∉ s
⊢ s = L.support.toFinset

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.LeAtTop
⊢ HasProd f (∏ b : β, f b) L

Tactic:
simpa using hasProd_fintype_support f L

Premises used: hasProd_fintype_support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter (↑(↑s : Set β) : Type u_2)
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : (↑(↑s : Set β) : Type u_2)) ↦ x ∈ L.support
⊢ HasProd (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (↑s : Set β)))
    (∏ b ∈ map (Embedding.subtype fun (x : β) ↦ x ∈ (↑s : Set β)) L.support.toFinset, f b) L

Tactic:
simpa [prod_attach] using hasProd_fintype_support (f ∘ Subtype.val) L

Premises used: hasProd_fintype_support, Function.comp, Finset.prod_attach, Subtype.val
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter (↑(↑s : Set β) : Type u_2)
inst_2 : L.LeAtTop
⊢ HasProd (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (↑s : Set β))) (∏ b ∈ s, f b) L

Tactic:
simpa [prod_attach, Embedding.subtype] using Finset.hasProd_support s f L

Premises used: Finset.hasProd_support, Function.Embedding.subtype, Finset.prod_attach
-- 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
h :
  ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
⊢ HasProd f (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b) L

Tactic:
apply tendsto_nhds_of_eventually_eq

Premises used: tendsto_nhds_of_eventually_eq