awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
⊢ Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ t0, g b))

Tactic:
tendsto_finsetProd _ fun b _ ↦ ?_

Premises used: tendsto_finsetProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
refine :
  ∀ b ∈ t0,
    Tendsto
      (fun (t : Finset ((b : β) × γ b)) ↦
        ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) b) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) b s))
      atTop (𝓝 (g b))
⊢ Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ t0, g b))

Tactic:
refine tendsto_finsetProd _ fun b _ ↦ ?_

Premises used: tendsto_finsetProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
b : β
h_1 : b ∈ t0
⊢ Tendsto
    (fun (t : Finset (Sigma γ)) ↦
      (fun (t : Finset (γ b)) ↦ (∏ s ∈ t, f (Sigma.mk (β := fun (b : β) ↦ γ b) b s) : α))
        (t.preimage (Sigma.mk (β := γ) b) ⋯))
    atTop (𝓝 (g b))

Tactic:
(hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, Filter.tendsto_finset_preimage_atTop_atTop, Filter.Tendsto.comp, sigma_mk_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
b : β
h_1 : b ∈ t0
⊢ Tendsto
    (fun (t : Finset (Sigma γ)) ↦
      (fun (t : Finset (γ b)) ↦ (∏ s ∈ t, f (Sigma.mk (β := fun (b : β) ↦ γ b) b s) : α))
        (t.preimage (Sigma.mk (β := γ) b) ⋯))
    atTop (𝓝 (g b))

Tactic:
exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))

Premises used: Filter.tendsto_finset_preimage_atTop_atTop, Filter.Tendsto.comp, sigma_mk_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
⊢ Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))

Tactic:
have L : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop
      (𝓝 <| ∏ b ∈ t0, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
⊢ ∃ (t : Finset ((b : β) × γ b)), ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v ∧ s ⊆ t

Tactic:
have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
    ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
this : ∃ (t : Finset ((b : β) × γ b)), ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v ∧ s ⊆ t
obtain :
  ∀ (t : Finset ((b : β) × γ b)) (tv : ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v) (st : s ⊆ t),
    ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
obtain ⟨t, tv, st⟩ := this
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v
st : s ⊆ t
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩

Premises used: Membership.mem, Sigma.fst, And.intro, Exists.intro, Finset.filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v
st : s ⊆ t
refine : ∀ (x : (b : β) × γ b) (hx : x ∈ s), x ∈ {p ∈ t | p.fst (β := fun (b : β) ↦ γ b) ∈ t0}
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
L :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v
st : s ⊆ t
x : (b : β) × γ b
hx : x ∈ s
⊢ x ∈ {p ∈ t | p.fst (β := fun (b : β) ↦ γ b) ∈ t0}

Tactic:
simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)

Premises used: Sigma.fst, Finset.mem_filter, Finset.mem_image_of_mem, true_and
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
ha : Multipliable f
b : β
⊢ Multipliable.{u_1, u_4} (α := α) fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)

Tactic:
ha.comp_injective sigma_mk_injective

Premises used: Multipliable.comp_injective, sigma_mk_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
ha : Multipliable f
⊢ Multipliable.{u_1, u_2} (α := α) fun (b : β) ↦ ∏' (c : γ b), f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)

Tactic:
ha.sigma' fun b ↦ ha.sigma_factor b

Premises used: Multipliable.sigma', Multipliable.sigma_factor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
f : β × γ → α
h : Multipliable f
b : β
⊢ Multipliable.{u_1, u_3} (α := α) fun (c : γ) ↦ f (b, c)

Tactic:
h.comp_injective fun _ _ h ↦ (Prod.ext_iff.1 h).2

Premises used: Prod.ext_iff, And.right, Multipliable.comp_injective, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
f : β × γ → α
h : Multipliable f
⊢ Multipliable.{u_1, u_2} (α := α) fun (b : β) ↦ ∏' (c : γ), f (b, c)

Tactic:
((Equiv.sigmaEquivProd β γ).multipliable_iff.mpr h).sigma

Premises used: Iff.mpr, Equiv.multipliable_iff, Multipliable.sigma, Equiv.sigmaEquivProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T2Space α
f : β → α
a : α
hf : HasProd f a
g : β → γ
⊢ HasProd (fun (c : γ) ↦ ∏' (b : (↑(g ⁻¹' {c}) : Type u_2)), f (↑b : β)) a

Tactic:
(((Equiv.sigmaFiberEquiv g).hasProd_iff).mpr hf).sigma <|
    fun _ ↦ ((hf.multipliable.subtype _).hasProd_iff).mpr rfl

Premises used: Iff.mpr, Multipliable.subtype, HasProd.sigma, Equiv.sigmaFiberEquiv, Equiv.hasProd_iff, Multipliable.hasProd_iff, HasProd.multipliable, Eq, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
γ : β → Type u_4
f : (b : β) × γ b → α
ha : Multipliable f
⊢ Eq.{u_1 + 1} (α := α) (∏' (p : (b : β) × γ b), f p) (∏' (b : β) (c : γ b), f (Sigma.mk (β := fun (b : β) ↦ γ b) b c))

Tactic:
Multipliable.tprod_sigma' (fun b ↦ ha.sigma_factor b) ha

Premises used: Multipliable.tprod_sigma', Multipliable.sigma_factor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : β × γ → α
h : Multipliable f
⊢ Eq.{u_1 + 1} (α := α) (∏' (p : β × γ), f p) (∏' (b : β) (c : γ), f (b, c))

Tactic:
h.tprod_prod' h.prod_factor

Premises used: Multipliable.prod_factor, Multipliable.tprod_prod'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : β → γ → α
h : Multipliable (uncurry f)
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ) (b : β), f b c) (∏' (b : β) (c : γ), f b c)

Tactic:
h.tprod_comm' h.prod_factor h.prod_symm.prod_factor

Premises used: Multipliable.prod_factor, Multipliable.prod_symm, Multipliable.tprod_comm'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
ι : Type u_4
X : α → Type u_5
inst : (x : α) → CommMonoid (X x)
inst_1 : (x : α) → TopologicalSpace (X x)
L : SummationFilter ι
f : ι → (x : α) → X x
g : (x : α) → X x
⊢ HasProd f g L ↔ ∀ (x : α), HasProd (fun (i : ι) ↦ f i x) (g x) L

Tactic:
simp only [HasProd, tendsto_pi_nhds, Finset.prod_apply]

Premises used: Finset.prod_apply, HasProd, tendsto_pi_nhds, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
ι : Type u_4
X : α → Type u_5
inst : (x : α) → CommMonoid (X x)
inst_1 : (x : α) → TopologicalSpace (X x)
L : SummationFilter ι
f : ι → (x : α) → X x
⊢ Multipliable f L ↔ ∀ (x : α), Multipliable.{u_5, u_4} (α := X x) (fun (i : ι) ↦ f i x) L

Tactic:
simp only [Multipliable, Pi.hasProd, Classical.skolem]

Premises used: Classical.skolem, Pi.hasProd, Multipliable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
ι : Type u_4
X : α → Type u_5
inst : (x : α) → CommMonoid (X x)
inst_1 : (x : α) → TopologicalSpace (X x)
L : SummationFilter ι
inst_2 : L.NeBot
inst_3 : ∀ (x : α), T2Space.{u_5} (X x)
f : ι → (x : α) → X x
x : α
hf : Multipliable f L
⊢ Eq.{u_5 + 1} (α := X x) ((∏'[L] (i : ι), f i) x) (∏'[L] (i : ι), f i x)

Tactic:
(Pi.hasProd.mp hf.hasProd x).tprod_eq.symm

Premises used: Pi.hasProd, HasProd.tprod_eq, Multipliable.hasProd, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
hf : HasSum f a L
⊢ HasSum (fun (a : β) ↦ MulOpposite.op (f a)) (MulOpposite.op a) L

Tactic:
(hf.map (@opAddEquiv α _) continuous_op :)

Premises used: HasSum.map, MulOpposite.opAddEquiv, MulOpposite.continuous_op, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → α
hf : Summable f L
⊢ Summable (MulOpposite.op ∘ f) L

Tactic:
hf.hasSum.op.summable

Premises used: HasSum.op, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → αᵐᵒᵖ
a : αᵐᵒᵖ
hf : HasSum f a L
⊢ HasSum (fun (a : β) ↦ MulOpposite.unop (f a)) (MulOpposite.unop a) L

Tactic:
(hf.map (@opAddEquiv α _).symm continuous_unop :)

Premises used: HasSum.map, MulOpposite.opAddEquiv, MulOpposite.continuous_unop, MulOpposite.unop, AddEquiv.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → αᵐᵒᵖ
hf : Summable f L
⊢ Summable (MulOpposite.unop ∘ f) L

Tactic:
hf.hasSum.unop.summable

Premises used: HasSum.unop, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
⊢ HasSum (fun (a : β) ↦ op (f a)) (op a) L ↔ HasSum f a L

Tactic:
⟨HasSum.unop, HasSum.op⟩

Premises used: HasSum.unop, HasSum.op, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → αᵐᵒᵖ
a : αᵐᵒᵖ
⊢ HasSum (fun (a : β) ↦ unop (f a)) (unop a) L ↔ HasSum f a L

Tactic:
⟨HasSum.op, HasSum.unop⟩

Premises used: HasSum.unop, HasSum.op, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → α
⊢ Summable.{u_1, u_2} (α := αᵐᵒᵖ) (fun (a : β) ↦ op (f a)) L ↔ Summable f L

Tactic:
⟨Summable.unop, Summable.op⟩

Premises used: Summable.unop, Iff.intro, Summable.op
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → αᵐᵒᵖ
⊢ Summable.{u_1, u_2} (α := α) (fun (a : β) ↦ unop (f a)) L ↔ Summable f L

Tactic:
⟨Summable.op, Summable.unop⟩

Premises used: Summable.unop, Iff.intro, Summable.op
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : T2Space α
⊢ Eq.{u_1 + 1} (α := αᵐᵒᵖ) (∑'[L] (x : β), op (f x)) (op (∑'[L] (x : β), f x))

Tactic:
(opHomeomorph.isClosedEmbedding.map_tsum f (g := opAddEquiv)).symm

Premises used: MulOpposite.opHomeomorph, Topology.IsClosedEmbedding.map_tsum, Homeomorph.isClosedEmbedding, Eq.symm, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
inst_2 : T2Space α
f : β → αᵐᵒᵖ
⊢ Eq.{u_1 + 1} (α := α) (∑'[L] (x : β), unop (f x)) (unop (∑'[L] (x : β), f x))

Tactic:
op_injective tsum_op.symm

Premises used: MulOpposite.op_injective, Eq.symm, tsum_op
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
inst_2 : StarAddMonoid α
inst_3 : ContinuousStar α
f : β → α
a : α
h : HasSum f a L
⊢ HasSum (fun (b : β) ↦ Star.star (f b)) (Star.star a) L

Tactic:
simpa only using h.map (starAddEquiv : α ≃+ α) continuous_star

Premises used: HasSum.map, ContinuousStar.continuous_star, starAddEquiv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
inst_2 : StarAddMonoid α
inst_3 : ContinuousStar α
f : β → α
hf : Summable f L
⊢ Summable.{u_1, u_2} (α := α) (fun (b : β) ↦ Star.star (f b)) L

Tactic:
hf.hasSum.star.summable

Premises used: HasSum.summable, HasSum.star, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
inst_2 : StarAddMonoid α
inst_3 : ContinuousStar α
f : β → α
hf : Summable.{u_1, u_2} (α := α) (fun (b : β) ↦ Star.star (f b)) L
⊢ Summable f L

Tactic:
simpa only [star_star] using hf.star

Premises used: star_star, Summable.star
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
inst_2 : StarAddMonoid α
inst_3 : ContinuousStar α
f : β → α
⊢ Summable.{u_1, u_2} (α := α) (fun (b : β) ↦ star (f b)) L ↔ Summable f L

Tactic:
⟨Summable.ofStar, Summable.star⟩

Premises used: Summable.ofStar, Summable.star, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
inst_2 : StarAddMonoid α
inst_3 : ContinuousStar α
f : β → α
⊢ Summable (star f) L ↔ Summable f L

Tactic:
summable_star_iff

Premises used: summable_star_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : AddCommMonoid α
inst_1 : TopologicalSpace α
inst_2 : StarAddMonoid α
inst_3 : ContinuousStar α
f : β → α
inst_4 : T2Space α
⊢ Eq.{u_1 + 1} (α := α) (star (∑'[L] (b : β), f b)) (∑'[L] (b : β), star (f b))

Tactic:
Function.LeftInverse.map_tsum (g := starAddEquiv) f continuous_star continuous_star star_star

Premises used: Function.LeftInverse.map_tsum, ContinuousStar.continuous_star, star_star
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
⊢ L.filter.NeBot

Tactic:
NeBot.ne_bot

Premises used: SummationFilter.NeBot.ne_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
pos : ∀ (h : L.filter = ⊥), L.NeBot ∨ L.filter = ⊥
neg : ∀ (h : ¬L.filter = ⊥), L.NeBot ∨ L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
by_cases h : L.filter = ⊥

Premises used: SummationFilter.filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
.inr h

Premises used: Or.inr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
exact .inr h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : ¬L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
.inl ⟨⟨h⟩⟩

Premises used: Filter.NeBot.mk, SummationFilter.NeBot.mk, Or.inl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : ¬L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
exact .inl ⟨⟨h⟩⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
⊢ L.support = (map SetLike.coe L.filter).limsInf

Tactic:
eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
refine : ∀ (c : Set β), L.support ≤ c ↔ (map SetLike.coe L.filter).limsInf ≤ c
⊢ L.support = (map SetLike.coe L.filter).limsInf

Tactic:
refine eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
c : Set β
hL : ∀ (t' : Set β), (∀ᶠ (a : Finset β) in L.filter, t' ⊆ (↑a : Set β)) → t' ⊆ c
x : β
hx : ∀ᶠ (s : Finset β) in L.filter, x ∈ s
⊢ ∀ᶠ (a : Finset β) in L.filter, {x} ⊆ (↑a : Set β)

Tactic:
simpa using hx