mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ liminf f F ≤ f m

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ x * (y + z) = x * y + x * z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
⊢ f F.limsSup = liminf f F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a ↔ HasProd f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ (y + z) * x = y * x + z * x

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ l (limsup v f) ≤ limsup (fun x ↦ l (v x)) f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ ∀ x ∉ Set.range fun a ↦ ↑a, f x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ a * b + a * -c = a * b - a * c

Tactic:
simp [← neg_mul, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ a * (b - c) = a * b - a * c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, a < b
⊢ liminf f (𝓝[>] a) = ⨆ r, ⨆ (_ : r > a), f r

Tactic:
by

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ b * a + -c * a = b * a - c * a

Tactic:
simp [← neg_mul, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ (b - c) * a = b * a - c * a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ ∀ i ∈ L.support, {s | i ∈ s} ∈ L.filter

Tactic:
by

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: n : ℕ
x : EReal
⊢ n • x = ↑n * x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ b, b < a
⊢ liminf f (𝓝[<] a) = ⨆ r, ⨆ (_ : r < a), f r

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
⊢ g (limsup u f) = limsup (fun x ↦ g (u x)) f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ b, a < b
⊢ limsup f (𝓝[>] a) = ⨅ r, ⨅ (_ : r > a), f r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ map (fun s ↦ ∏ b ∈ s, f b) atTop ≤ map (fun s ↦ ∏ x ∈ s, g x) atTop

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, b < a
⊢ limsup f (𝓝[<] a) = ⨅ r, ⨅ (_ : r < a), f r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd f (∏ b ∈ L.support.toFinset, f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Fintype β
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ HasProd f (∏ b, f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ map (Embedding.subtype fun x ↦ x ∈ ↑s) L.support.toFinset, f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝ : L.LeAtTop
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
x✝ : α
⊢ x✝ ∈ {x | (fun a ↦ u a < b) x} ∩ {x | (fun a ↦ v a < b) x} → x✝ ∈ {x | (fun a ↦ max (u a) (v a) < b) x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop = Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ limsup (fun a ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
⊢ ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd f (∏ b ∈ (↑s ∩ L.support).toFinset, f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst✝ : L.HasSupport
⊢ Multipliable f L

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f = s.sup' hs fun i ↦ limsup (F i) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup fun i ↦ limsup (F i) f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ∀ x ∈ ⋯.toFinset, L.support.mulIndicator (fun b ↦ f b) x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f (∏'[L] (b : β), f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a₁ a₂ : α
⊢ HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a : α
h : HasProd f a L
⊢ HasProd (fun b ↦ (f b)⁻¹) a⁻¹ L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
hf : Multipliable (fun b ↦ (f b)⁻¹) L
⊢ Multipliable f L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ HasProd (fun b ↦ f b / g b) (a₁ / a₂) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hg : Multipliable g L
hfg : Multipliable (fun b ↦ f b / g b) L
⊢ Multipliable f L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hfg : Multipliable (fun b ↦ f b / g b) L
hf : Multipliable f L
⊢ Multipliable (fun b ↦ g b / f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
⊢ HasProd (Function.update f b a) (a / f b * a₁) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
⊢ HasProd (f ∘ Subtype.val) a₂ ↔ HasProd f (a₁ * a₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ HasProd (fun x ↦ 1) 1 L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
⊢ HasProd f (a₁ * (a₂ / a₁)) ↔ HasProd f a₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : IsEmpty β
⊢ HasProd f 1 L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : Subsingleton α
⊢ HasProd f 1 L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a : α
s : Finset β
⊢ HasProd f ((∏ b ∈ s, f b) * a) ↔ HasProd f (a * ∏ i ∈ s, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd (extend g f 1) a ↔ HasProd f a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ HasProd (fun n ↦ if n = b then 1 else f n) (a / f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
⊢ Multipliable (f ∘ Subtype.val)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hf : Multipliable f
hfg : f =ᶠ[cofinite] g
⊢ ∀ (b : ↑{x | (fun x ↦ f x = g x) x}ᶜᶜ), (f ∘ Subtype.val) b = (g ∘ Subtype.val) b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.HasSupport
h : HasFiniteMulSupport f
⊢ Multipliable f L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
L : SummationFilter β
inst✝ : L.LeAtTop
this : HasProd f (∏ b' ∈ {b}, f b') L
⊢ HasProd f (f b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : α
L : SummationFilter β
inst✝ : L.LeAtTop
this : HasProd (fun b' ↦ if b' = b then a else 1) (if b = b then a else 1) L
⊢ HasProd (fun b' ↦ if b' = b then a else 1) a L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommMonoid α
inst✝ : CompleteSpace α
f : β → α
⊢ Multipliable f ↔ CauchySeq fun s ↦ ∏ b ∈ s, f b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : α
L : SummationFilter β
inst✝ : L.LeAtTop
this : HasProd (fun b' ↦ if b = b' then a else 1) (if b = b then a else 1) L
⊢ HasProd (fun b' ↦ if b = b' then a else 1) a L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
e : γ ≃ β
⊢ ∀ x ∉ Set.range ⇑e, f x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
⊢ HasProd f a ↔ HasProd g a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous[inst✝⁴, inst✝²] ⇑g
⊢ HasProd (⇑g ∘ f) (g a) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : CommMonoid α
inst✝⁶ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst✝⁶, inst✝⁴] ⇑g
hg' : Continuous[inst✝⁴, inst✝⁶] ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f) L
⊢ Multipliable f L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
b : α'
hb : Tendsto (fun s ↦ ∏ x ∈ s, g (f x)) L.filter (𝓝 b)
⊢ ∀ (x : Finset ι), ∏ x ∈ x, g (f x) ∈ Set.range ⇑g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ⊆ (t₁, t₂).1
ht₂ : (s, s).2 ⊆ (t₁, t₂).2
⊢ (∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (CauchySeq fun s ↦ ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
by

Goal state after: