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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ n ∈ {n | b'' < u n r}

Tactic:
by

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ L.support = (map SetLike.coe L.filter).limsInf

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ Finite ↑{n | b'' < u n r}

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 : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ liminf u f ≤ limsup v f

Tactic:
by

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b ∈ s
this : ⋂ i ∈ t, {x | (fun s ↦ i ∈ s) x} ∈ L.filter
r : Finset β
hr : r ∈ ⋂ i ∈ t, {x | (fun s ↦ i ∈ s) x}
⊢ t ⊆ r

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ rs ↑⟨n, hn⟩ ≤ ⨆ n, rs ↑n

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
by

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
⊢ ∀ (a : Finset β), {b} ⊆ a → b ∈ a

Tactic:
by

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ L.support = univ ↔ L.filter ≤ atTop

Tactic:
by

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.support = univ

Tactic:
by

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.LeAtTop

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
b : β
⊢ (fun x ↦ x ∈ L.support) b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ᶠ (s : Finset β) in L.filter, ↑s ⊆ L.support

Tactic:
by

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
⊢ (∀ᶠ (s : Finset β) in L.filter, b ∈ s) ∨ ∀ᶠ (s : Finset β) in L.filter, b ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
hc' : c ∈ (L.map f).support
this : ∃ x, Finset.map f x ∈ {x | (fun s ↦ c ∈ s) x}
⊢ c ∈ ⇑f '' L.support

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ -x * y = -(x * y)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
⊢ c ∈ ⇑f '' L.support → c ∈ (L.map f).support

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ x * -y = -(x * y)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
⊢ (L.map f).support = ⇑f '' L.support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : β ↪ γ
h : L.NeBot
a : Finset β
⊢ ↑a ⊆ L.support → ↑a ⊆ ⇑f ⁻¹' ⇑f '' L.support

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

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 : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∈ m
⊢ j = liminfReparam f s p j

Tactic:
by

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

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ℕ → α → β
c : β
h_all : ∀ (n : ℕ), Tendsto (u n) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun n ↦ u n r) atTop) atTop (𝓝 c)
h_anti : ∀ (n : ℕ), Antitone (u n)
⊢ Tendsto (fun r ↦ ⨆ n, u n r) atTop (𝓝 c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : β ↪ γ
⊢ (L.map f).HasSupport

Tactic:
by

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
f : γ ↪ β
⊢ (L.comap f).support = ⇑f ⁻¹' L.support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : γ ↪ β
⊢ (L.comap f).HasSupport

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
f : γ ↪ β
⊢ (L.comap f).filter ≤ atTop

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage ⇑f ⋯ ∈ s
⊢ InjOn (⇑f) (⇑f ⁻¹' ↑t)

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤

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 : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ (unconditional β).comap f = unconditional γ

Tactic:
by

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

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
this : Fintype β
⊢ atTop = pure Finset.univ

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
by

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

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
⊢ L = unconditional β

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
⊢ (conditional β).support = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder β
inst✝² : Nonempty β
inst✝¹ : IsDirectedOrder β
inst✝ : IsCodirectedOrder β
⊢ (conditional β).filter.NeBot

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
by

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

Goal state before:
pp: γ : Type u_4
inst✝² : PartialOrder γ
inst✝¹ : LocallyFiniteOrder γ
inst✝ : OrderBot γ
⊢ (conditional γ).filter = Filter.map Finset.Iic atTop

Tactic:
by

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

Goal state before:
pp: γ : Type u_4
inst✝² : PartialOrder γ
inst✝¹ : LocallyFiniteOrder γ
inst✝ : OrderTop γ
⊢ (conditional γ).filter = Filter.map Finset.Ici atBot

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Finset.Iic n = Finset.range (n + 1)

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 : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∉ m
⊢ ∃ n, ⋯.choose n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

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
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∃ᶠ (n : R) in F, F.limsSup ≤ n

Tactic:
by

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

Goal state before:
pp: this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ a ≤ b + 1

Tactic:
by

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

Goal state before:
pp: this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ a ≤ b - 1

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 : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
⊢ ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)

Tactic:
by

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

Goal state before:
pp: this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ Finset.range b ∈ s

Tactic:
by

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

Goal state before:
pp: ⊢ (conditional ℕ).filter = Filter.map Finset.range atTop

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
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
⊢ ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ {x | f x < liminf f 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 β
hL : ¬L.NeBot
f : β → α
a : α
⊢ L.filter = ⊥

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

Tactic:
rw [HasProd, this]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
⊢ Tendsto (fun s ↦ ∏ b ∈ s, f b) ⊥ (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
⊢ HasProd f a 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 β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ ¬(L.HasSupport ∧ (mulSupport fun b ↦ f b).Finite)

Tactic:
by

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

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal

Tactic:
by

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

Goal state before:
pp: x y : EReal
hy : 0 ≤ y
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal

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 β
hL : ¬L.NeBot
f : β → α
⊢ ∏'[L] (b : β), f b = ∏ᶠ (b : β), f b

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 : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
H : ∃ j, BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

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
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}
⊢ (Set.Ioo l F.limsSup).Nonempty

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 : β → α
h : ¬Multipliable f L
⊢ ∏'[L] (b : β), f b = 1

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 : α
L : SummationFilter γ
g : γ → β
hg : Injective g
⊢ HasProd f a (L.map { toFun := g, inj' := hg }) ↔ HasProd (f ∘ g) a L

Tactic:
by

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c

Tactic:
by

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ c * (a + b) = c * a + c * b

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
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:
apply liminf_le_of_frequently_le _ _

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

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.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
hb : 0 ≤ b
hc : c ≤ 0
⊢ 0 ≤ -c

Tactic:
by

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

Goal state before:
pp: a b c : EReal
hb : 0 ≤ b
hc : c ≤ 0
⊢ 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
hb : 0 ≤ b
hc : c ≤ 0
⊢ a * (b - c) = a * b - a * c

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

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 : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, 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: