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
⊢ ∃ᶠ (i : R) in F, f i ≤ f m

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
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f

Tactic:
·

Goal state after:
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
⊢ ∃ᶠ (i : R) in F, f i ≤ f m
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
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f

Tactic:
·

Goal state after:
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
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.hs
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), (s ↑j).Nonempty

pp: case neg.H
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∃ j, BddBelow (range fun i ↦ f ↑i)

Tactic:
·

Goal state after:
case neg.hs
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), (s ↑j).Nonempty
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.H
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∃ j, BddBelow (range fun i ↦ f ↑i)

Tactic:
·

Goal state after:
case neg.H
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∃ j, BddBelow (range fun i ↦ f ↑i)
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : 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
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f (g b)

pp: case a
α : 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
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b

Tactic:
·

Goal state after:
case a
α : 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
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f (g b)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : 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)
⊢ limsup (fun a ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)

pp: case a
α : 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)
⊢ max (limsup u f) (limsup v f) ≤ limsup (fun a ↦ max (u a) (v a)) f

Tactic:
·

Goal state after:
case a
α : 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)
⊢ limsup (fun a ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : 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
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ ∀ x ∈ image g t ∪ s, x ∉ image g t → f x = 1

Tactic:
simp only [Finset.mem_union, Finset.mem_image]

Goal state after:
case a
α : 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
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ ∀ (x : β), (∃ a ∈ t, g a = x) ∨ x ∈ s → (¬∃ a ∈ t, g a = x) → f x = 1
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : 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
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b

Tactic:
·

Goal state after:
case a
α : 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
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : 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)
⊢ max (limsup u f) (limsup v f) ≤ limsup (fun a ↦ max (u a) (v a)) f

Tactic:
·

Goal state after:
case a
α : 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)
⊢ max (limsup u f) (limsup v f) ≤ limsup (fun a ↦ max (u a) (v a)) f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : 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
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f ≤ s.sup' hs fun i ↦ limsup (F i) f

pp: case a
α : 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
⊢ (s.sup' hs fun i ↦ limsup (F i) f) ≤ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f

Tactic:
·

Goal state after:
case a
α : 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
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f ≤ s.sup' hs fun i ↦ limsup (F i) f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : 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
⊢ (s.sup' hs fun i ↦ limsup (F i) f) ≤ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f

Tactic:
·

Goal state after:
case a
α : 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
⊢ (s.sup' hs fun i ↦ limsup (F i) f) ≤ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f
Module: Mathlib.Order.LiminfLimsup

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

pp: case inr
α : 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)
h✝ : f.NeBot
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup fun i ↦ limsup (F i) f

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ (F i)
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) ⊥ = s.sup fun i ↦ limsup (F i) ⊥
Module: Mathlib.Order.LiminfLimsup

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

pp: case inr.inr
α : 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)
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup fun i ↦ limsup (F i) f

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
h✝ : f.NeBot
h₁ : ∀ i ∈ ∅, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ ∅, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ limsup (fun a ↦ ∅.sup fun i ↦ F i a) f = ∅.sup fun i ↦ limsup (F i) f
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos
α : 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
⊢ HasProd f (finprod (L.support.mulIndicator fun b ↦ f b)) L

pp: case pos
α : 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)
h' : HasProd (fun b ↦ f b) 1 L
⊢ HasProd f 1 L

pp: case neg
α : 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)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L

Tactic:
·

Goal state after:
case pos
α : 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
⊢ HasProd f (finprod (L.support.mulIndicator fun b ↦ f b)) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case e'_6
α : 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
⊢ finprod (L.support.mulIndicator fun b ↦ f b) = ∏ b ∈ (↑⋯.toFinset ∩ L.support).toFinset, f b

pp: case pos.convert_5
α : 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
⊢ ∀ b ∈ L.support, b ∉ ⋯.toFinset → f b = 1

pp: case pos.convert_6
α : 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
⊢ L.HasSupport

Tactic:
·

Goal state after:
case e'_6
α : 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
⊢ finprod (L.support.mulIndicator fun b ↦ f b) = ∏ b ∈ (↑⋯.toFinset ∩ L.support).toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case e'_6
α : 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
⊢ ∏ i ∈ ⋯.toFinset, L.support.mulIndicator (fun b ↦ f b) i = ∏ b ∈ ⋯.toFinset, f b

pp: case e'_6.h
α : 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
⊢ mulSupport (L.support.mulIndicator fun b ↦ f b) ⊆ ↑⋯.toFinset

Tactic:
·

Goal state after:
case e'_6
α : 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
⊢ ∏ i ∈ ⋯.toFinset, L.support.mulIndicator (fun b ↦ f b) i = ∏ b ∈ ⋯.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case e'_6.h
α : 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
⊢ mulSupport (L.support.mulIndicator fun b ↦ f b) ⊆ ↑⋯.toFinset

Tactic:
·

Goal state after:
case e'_6.h
α : 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
⊢ mulSupport (L.support.mulIndicator fun b ↦ f b) ⊆ ↑⋯.toFinset
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos.convert_5
α : 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
⊢ ∀ b ∈ L.support, b ∉ ⋯.toFinset → f b = 1

pp: case pos.convert_6
α : 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
⊢ L.HasSupport

Tactic:
·

Goal state after:
case pos.convert_5
α : 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
⊢ ∀ b ∈ L.support, b ∉ ⋯.toFinset → f b = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos.convert_6
α : 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
⊢ L.HasSupport

Tactic:
·

Goal state after:
case pos.convert_6
α : 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
⊢ L.HasSupport
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos
α : 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)
h' : HasProd (fun b ↦ f b) 1 L
⊢ HasProd f 1 L

pp: case neg
α : 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)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L

Tactic:
·

Goal state after:
case pos
α : 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)
h' : HasProd (fun b ↦ f b) 1 L
⊢ HasProd f 1 L
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case neg
α : 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)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L

Tactic:
·

Goal state after:
case neg
α : 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)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case pos
α : 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 : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

pp: case neg
α : 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 : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
·

Goal state after:
case pos
α : 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 : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case neg
α : 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 : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
·

Goal state after:
case neg
α : 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 : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case e'_5
α : 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 : β
⊢ (fun n ↦ if n = b then 1 else f n) = update f b 1

pp: case e'_6
α : 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 : β
⊢ a / f b = 1 / f b * a

Tactic:
·

Goal state after:
case e'_5
α : 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 : β
⊢ (fun n ↦ if n = b then 1 else f n) = update f b 1