awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ Subset (α := Set γ) (mulSupport.{u_3, u_1} (M := α) fun (d : γ) ↦ (s d).mulIndicator f i) {j}

Tactic:
Set.mulSupport_subset_subsingleton_of_disjoint_on_mulSupport f hs i j hj

Premises used: Set.mulSupport_subset_subsingleton_of_disjoint_on_mulSupport
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ Subset (α := Set γ) (mulSupport.{u_3, u_1} (M := α) fun (d : γ) ↦ (s d).mulIndicator f i) {j}

Tactic:
exact Set.mulSupport_subset_subsingleton_of_disjoint_on_mulSupport f hs i j hj

Premises used: Set.mulSupport_subset_subsingleton_of_disjoint_on_mulSupport
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise (Disjoint on s)
i : β
hi : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i
⊢ ∏' (d : γ), (s d).mulIndicator f i = f i

Tactic:
tprod_mulIndicator_of_disjoint_on_mulSupport_of_mem s f i hi (pairwise_disjoint_mono hs
    <| fun _ _ hi ↦ hi.1)

Premises used: pairwise_disjoint_mono, tprod_mulIndicator_of_disjoint_on_mulSupport_of_mem, And.left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : ∀ (d : γ), i ∉ s d
⊢ Eq.{u_1 + 1} (α := α) (∏' (d : γ), (s d).mulIndicator f i) 1

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : β
pos :
  ∀ (h₀ : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i),
    Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
neg : ∀ (h₀ : i ∉ ⋃ (d : γ), s d), Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
⊢ Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
by_cases h₀ : i ∈ ⋃ d, s d
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : β
h₀ : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i
⊢ Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
simp only [h₀, hs, Set.mulIndicator_of_mem, tprod_mulIndicator_of_disjoint_on_mulSupport_of_mem]

Premises used: tprod_mulIndicator_of_disjoint_on_mulSupport_of_mem, Set.mulIndicator_of_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : β
h₀ : i ∉ ⋃ (d : γ), s d
⊢ Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
hs : Pairwise (Disjoint on s)
f : β → α
h : ∀ (i : β), Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
⊢ Set.mulIndicator (⋃ (d : γ), s d) f = fun (i : β) ↦ ∏' (d : γ), (s d).mulIndicator f i

Tactic:
ext i
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
hs : Pairwise (Disjoint on s)
f : β → α
i : β
⊢ Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
mulIndicator_iUnion_of_pairwise_disjoint_on_mulSupport s f (pairwise_disjoint_mono hs
    <| fun _ _ hi ↦ hi.1) i

Premises used: pairwise_disjoint_mono, mulIndicator_iUnion_of_pairwise_disjoint_on_mulSupport, And.left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
hs : Pairwise (Disjoint on s)
f : β → α
i : β
⊢ Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
exact mulIndicator_iUnion_of_pairwise_disjoint_on_mulSupport s f (pairwise_disjoint_mono hs
    <| fun _ _ hi ↦ hi.1) i

Premises used: pairwise_disjoint_mono, mulIndicator_iUnion_of_pairwise_disjoint_on_mulSupport, And.left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : T2Space α
α' : Type u_4
inst_3 : CommMonoid α'
inst_4 : TopologicalSpace α'
e : α' → α
hes : Surjective e
h1 : e 1 = 1
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
hg : ¬Multipliable g
⊢ ¬Multipliable f

Tactic:
have hf : ¬Multipliable f := mt (hes.multipliable_iff_of_hasProd_iff @h).1 hg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : T2Space α
α' : Type u_4
inst_3 : CommMonoid α'
inst_4 : TopologicalSpace α'
e : α' → α
hes : Surjective e
h1 : e 1 = 1
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
hg : ¬Multipliable g
hf : ¬Multipliable f
⊢ ∏' (b : β), f b = e (∏' (c : γ), g c)

Tactic:
simp [tprod_def, hf, hg, h1]

Premises used: tprod_def
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : T2Space α
f : β → α
g : γ → α
h : ∀ {a : α}, HasProd f a ↔ HasProd g a
⊢ Eq.{u_1 + 1} (α := α) (∏' (b : β), f b) (∏' (c : γ), g c)

Tactic:
surjective_id.tprod_eq_tprod_of_hasProd_iff_hasProd rfl @h

Premises used: Function.surjective_id, Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : L.NeBot
hf : Multipliable f L
hg : Multipliable g L
⊢ ∏'[L] (b : β), f b * g b = HMul.hMul (α := α) (∏'[L] (b : β), f b) (∏'[L] (b : β), g b)

Tactic:
(hf.hasProd.mul hg.hasProd).tprod_eq

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : L.NeBot
hf : Multipliable f L
⊢ ∏'[L] (b : β), HPow.hPow (β := ℕ) (f b) 0 = HPow.hPow (α := α) (β := ℕ) (∏'[L] (b : β), f b) 0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : L.NeBot
hf : Multipliable f L
n : ℕ
hn : ∏'[L] (b : β), f b ^ n = HPow.hPow (α := α) (∏'[L] (b : β), f b) n
⊢ ∏'[L] (b : β), f b ^ (n + 1) = HPow.hPow (α := α) (∏'[L] (b : β), f b) (n + 1)

Tactic:
simp [pow_succ, (hf.pow n).tprod_mul hf, hn]

Premises used: pow_succ, Multipliable.pow, Multipliable.tprod_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : L.NeBot
hf : Multipliable f L
n : ℕ
zero : ∏'[L] (b : β), HPow.hPow (β := ℕ) (f b) 0 = HPow.hPow (α := α) (β := ℕ) (∏'[L] (b : β), f b) 0
succ :
  ∀ (n : ℕ) (hn : ∏'[L] (b : β), f b ^ n = HPow.hPow (α := α) (∏'[L] (b : β), f b) n),
    ∏'[L] (b : β), f b ^ (n + 1) = HPow.hPow (α := α) (∏'[L] (b : β), f b) (n + 1)
⊢ ∏'[L] (b : β), f b ^ n = HPow.hPow (α := α) (∏'[L] (b : β), f b) n

Tactic:
induction n with
  | zero => simp
  | succ n hn => simp [pow_succ, (hf.pow n).tprod_mul hf, hn]

Premises used: pow_succ, Multipliable.pow, Multipliable.tprod_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : L.NeBot
f : γ → β → α
s : Finset γ
hf : ∀ i ∈ s, Multipliable (f i) L
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), ∏ i ∈ s, f i b) (∏ i ∈ s, ∏'[L] (b : β), f i b)

Tactic:
(hasProd_prod fun i hi ↦ (hf i hi).hasProd).tprod_eq

Premises used: hasProd_prod, HasProd.tprod_eq, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
n : β
pos : ∀ (h : n = b), f n = f n * update (β := fun (a : β) ↦ α) f b 1 n
neg : ∀ (h : ¬n = b), f n = 1 * update (β := fun (a : β) ↦ α) f b 1 n
⊢ f n = (if n = b then f n else 1) * update (β := fun (a : β) ↦ α) f b 1 n

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
n : β
h : n = b
⊢ f n = f n * update (β := fun (a : β) ↦ α) f b 1 n

Tactic:
simp [update_apply, h]

Premises used: Function.update_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
n : β
h : ¬n = b
⊢ f n = 1 * update (β := fun (a : β) ↦ α) f b 1 n

Tactic:
simp [update_apply, h]

Premises used: Function.update_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
e_a : (∏'[L] (x : β), if x = b then f x else 1) = if b = b then f b else 1
⊢ HMul.hMul (α := α) (∏'[L] (x : β), if x = b then f x else 1) (∏'[L] (x : β), update (β := fun (a : β) ↦ α) f b 1 x) =
    (if b = b then f b else 1) * ∏'[L] (x : β), update (β := fun (a : β) ↦ α) f b 1 x

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
⊢ (∏'[L] (x : β), if x = b then f x else 1) = if b = b then f b else 1

Tactic:
tprod_eq_mulSingle b fun b' hb' ↦ if_neg hb'

Premises used: tprod_eq_mulSingle, if_neg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
⊢ (∏'[L] (x : β), if x = b then f x else 1) = if b = b then f b else 1

Tactic:
exact tprod_eq_mulSingle b fun b' hb' ↦ if_neg hb'

Premises used: tprod_eq_mulSingle, if_neg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
⊢ (if b = b then f b else 1) * ∏'[L] (x : β), update (β := fun (a : β) ↦ α) f b 1 x =
    f b * ∏'[L] (x : β), if x = b then 1 else f x

Tactic:
simp only [update, if_true, eq_rec_constant, dite_eq_ite]

Premises used: Function.update, if_true, eq_rec_constant, dite_eq_ite
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : T2Space α
inst_3 : ContinuousMul α
s : Set β
hs : Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
hsc : Multipliable (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ))
⊢ HMul.hMul (α := α) (∏' (x : (↑s : Type u_2)), f (↑x : β)) (∏' (x : (↑sᶜ : Type u_2)), f (↑x : β)) = ∏' (x : β), f x

Tactic:
(hs.hasProd.mul_compl hsc.hasProd).tprod_eq.symm

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.mul_compl, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : T2Space α
inst_3 : ContinuousMul α
s t : Set β
hd : Disjoint s t
hs : Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
ht : Multipliable (β := (↑t : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ t))
⊢ ∏' (x : (↑(s ∪ t) : Type u_2)), f (↑x : β) =
    HMul.hMul (α := α) (∏' (x : (↑s : Type u_2)), f (↑x : β)) (∏' (x : (↑t : Type u_2)), f (↑x : β))

Tactic:
(hs.hasProd.mul_disjoint hd ht.hasProd).tprod_eq

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.mul_disjoint
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : T2Space α
inst_3 : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
hd : (↑s : Set ι).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, Multipliable (β := (↑(t i) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ t i))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(⋃ i ∈ s, t i) : Type u_2)), f (↑x : β))
    (∏ i ∈ s, ∏' (x : (↑(t i) : Type u_2)), f (↑x : β))

Tactic:
(hasProd_prod_disjoint _ hd fun i hi ↦ (hf i hi).hasProd).tprod_eq

Premises used: HasProd.tprod_eq, Multipliable.hasProd, hasProd_prod_disjoint
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
hf : ∃ (b : β), f b = 0
inst_2 : L.LeAtTop
obtain : ∀ (b : β) (hb : f b = 0), HasProd f 0 L
⊢ HasProd f 0 L

Tactic:
obtain ⟨b, hb⟩ := hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
b : β
hb : f b = 0
apply : EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ 0) fun (s : Finset β) ↦ ∏ b ∈ s, f b
⊢ HasProd f 0 L

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
b : β
hb : f b = 0
h : ∀ (s : Finset β) (hs : {b} ≤ s), Eq.{u_1 + 1} (α := α) 0 (∏ b ∈ s, f b)
⊢ EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ 0) fun (s : Finset β) ↦ ∏ b ∈ s, f b

Tactic:
filter_upwards [(eventually_ge_atTop {b}).filter_mono L.le_atTop] with s hs

Premises used: Filter.Eventually.filter_mono, Filter.eventually_ge_atTop, SummationFilter.LeAtTop.le_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
b : β
hb : f b = 0
s : Finset β
hs : {b} ≤ s
⊢ Eq.{u_1 + 1} (α := α) 0 (∏ b ∈ s, f b)

Tactic:
(Finset.prod_eq_zero (Finset.singleton_subset_iff.mp hs) hb).symm

Premises used: Finset.singleton_subset_iff, Finset.prod_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
b : β
hb : f b = 0
s : Finset β
hs : {b} ≤ s
⊢ Eq.{u_1 + 1} (α := α) 0 (∏ b ∈ s, f b)

Tactic:
exact (Finset.prod_eq_zero (Finset.singleton_subset_iff.mp hs) hb).symm

Premises used: Finset.singleton_subset_iff, Finset.prod_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
hf : ∃ (b : β), f b = 0
inst_2 : L.LeAtTop
⊢ Multipliable f L

Tactic:
⟨0, hasProd_zero_of_exists_eq_zero hf⟩

Premises used: Multipliable, hasProd_zero_of_exists_eq_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : L.NeBot
inst_4 : L.LeAtTop
hf : ∃ (b : β), f b = 0
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) 0

Tactic:
(hasProd_zero_of_exists_eq_zero hf).tprod_eq

Premises used: HasProd.tprod_eq, hasProd_zero_of_exists_eq_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G : Type u_1
inst : Neg G
inst_1 : Preorder G
inst_2 : LocallyFiniteOrder G
inst_3 : Filter.NeBot.{u_1} (α := G) atTop
⊢ (symmetricIcc G).filter.NeBot

Tactic:
simp [symmetricIcc, Filter.NeBot.map]

Premises used: SummationFilter.symmetricIcc, Filter.NeBot.map
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G : Type u_1
inst : Neg G
inst_1 : Preorder G
inst_2 : LocallyFiniteOrder G
inst_3 : Filter.NeBot.{u_1} (α := G) atTop
⊢ (symmetricIco G).filter.NeBot

Tactic:
simp [symmetricIco, Filter.NeBot.map]

Premises used: SummationFilter.symmetricIco, Filter.NeBot.map
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G : Type u_1
inst : Neg G
inst_1 : Preorder G
inst_2 : LocallyFiniteOrder G
inst_3 : Filter.NeBot.{u_1} (α := G) atTop
⊢ (symmetricIoc G).filter.NeBot

Tactic:
simp [symmetricIoc, Filter.NeBot.map]

Premises used: Filter.NeBot.map, SummationFilter.symmetricIoc
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G : Type u_1
inst : Neg G
inst_1 : Preorder G
inst_2 : LocallyFiniteOrder G
inst_3 : Filter.NeBot.{u_1} (α := G) atTop
⊢ (symmetricIoo G).filter.NeBot

Tactic:
simp [symmetricIoo, Filter.NeBot.map]

Premises used: Filter.NeBot.map, SummationFilter.symmetricIoo
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
⊢ (symmetricIcc G).filter ≤ (conditional G).filter

Tactic:
Filter.map_mono (tendsto_neg_atTop_atBot.prodMk tendsto_id)

Premises used: Filter.map_mono, Set.Mem, Filter.tendsto_id, setOf, Filter.tendsto_neg_atTop_atBot, Finset.Icc, Set.Subset, Set.preimage, Filter.Tendsto.prodMk
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G_1 : Type u_1
inst : Neg G_1
inst_1 : Preorder G_1
inst_2 : LocallyFiniteOrder G_1
inst_3 : Filter.NeBot.{u_1} (α := G_1) atTop
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : PartialOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : NoTopOrder G
inst_9 : NoBotOrder G
⊢ Tendsto (β := Finset G) (fun (N : G) ↦ Ico (-N) N) atTop atTop

Tactic:
tendsto_Ico_neg_atTop_atTop

Premises used: Finset.tendsto_Ico_neg_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G_1 : Type u_1
inst : Neg G_1
inst_1 : Preorder G_1
inst_2 : LocallyFiniteOrder G_1
inst_3 : Filter.NeBot.{u_1} (α := G_1) atTop
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : PartialOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : NoTopOrder G
inst_9 : NoBotOrder G
⊢ Tendsto (β := Finset G) (fun (N : G) ↦ Ico (-N) N) atTop atTop

Tactic:
exact tendsto_Ico_neg_atTop_atTop

Premises used: Finset.tendsto_Ico_neg_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G_1 : Type u_1
inst : Neg G_1
inst_1 : Preorder G_1
inst_2 : LocallyFiniteOrder G_1
inst_3 : Filter.NeBot.{u_1} (α := G_1) atTop
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : PartialOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : NoTopOrder G
inst_9 : NoBotOrder G
⊢ Tendsto (β := Finset G) (fun (N : G) ↦ Ioc (-N) N) atTop atTop

Tactic:
tendsto_Ioc_neg_atTop_atTop

Premises used: Finset.tendsto_Ioc_neg_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G_1 : Type u_1
inst : Neg G_1
inst_1 : Preorder G_1
inst_2 : LocallyFiniteOrder G_1
inst_3 : Filter.NeBot.{u_1} (α := G_1) atTop
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : PartialOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : NoTopOrder G
inst_9 : NoBotOrder G
⊢ Tendsto (β := Finset G) (fun (N : G) ↦ Ioc (-N) N) atTop atTop

Tactic:
exact tendsto_Ioc_neg_atTop_atTop

Premises used: Finset.tendsto_Ioc_neg_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G_1 : Type u_1
inst : Neg G_1
inst_1 : Preorder G_1
inst_2 : LocallyFiniteOrder G_1
inst_3 : Filter.NeBot.{u_1} (α := G_1) atTop
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : PartialOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : NoTopOrder G
inst_9 : NoBotOrder G
⊢ Tendsto (β := Finset G) (fun (g : G) ↦ Ioo (-g) g) atTop atTop

Tactic:
tendsto_Ioo_neg_atTop_atTop

Premises used: Finset.tendsto_Ioo_neg_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
G_1 : Type u_1
inst : Neg G_1
inst_1 : Preorder G_1
inst_2 : LocallyFiniteOrder G_1
inst_3 : Filter.NeBot.{u_1} (α := G_1) atTop
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : PartialOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : NoTopOrder G
inst_9 : NoBotOrder G
⊢ Tendsto (β := Finset G) (fun (g : G) ↦ Ioo (-g) g) atTop atTop

Tactic:
exact tendsto_Ioo_neg_atTop_atTop

Premises used: Finset.tendsto_Ioo_neg_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
⊢ (symmetricIcc ℤ).filter = Filter.map (fun (N : ℕ) ↦ Icc (-(↑N : ℤ)) (↑N : ℤ)) atTop

Tactic:
simp [← Nat.map_cast_int_atTop, Function.comp_def]

Premises used: Function.comp_def, Nat.map_cast_int_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
simp :
  Eq (α := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Icc (-g) g) atTop)
    (Filter.map (fun (g : ℤ) ↦ Ioo (-g) g) atTop)
⊢ symmetricIcc ℤ = symmetricIoo ℤ

Tactic:
simp only [symmetricIcc, symmetricIoo, mk.injEq]

Premises used: SummationFilter.symmetricIcc, SummationFilter.symmetricIoo, SummationFilter.mk.injEq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
h :
  ∀ (s : Set (Finset ℤ)),
    Membership.mem (γ := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Icc (-g) g) atTop) s ↔
      Membership.mem (γ := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Ioo (-g) g) atTop) s
⊢ Eq (α := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Icc (-g) g) atTop)
    (Filter.map (fun (g : ℤ) ↦ Ioo (-g) g) atTop)

Tactic:
ext s