mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
⊢ 0 ≤ U

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
l : Filter γ
u : γ → α
a : α
⊢ (∀ᶠ (x : β) in map (fun x ↦ e (u x)) l, (fun x1 x2 ↦ x1 ≤ x2) x (e a)) ↔
    ∀ᶠ (x : α) in map u l, (fun x1 x2 ↦ x1 ≤ x2) x a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (g ∘ f) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u ∨ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
⊢ ∃ᶠ (x' : S) in map f F, f l ≤ x'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_incr : Monotone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_decr : Antitone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x2 ≤ x1) F
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SupConvergenceClass α

Tactic:
refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩
  · rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
    lift c to s using hcs
    exact (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx
  · exact Eventually.of_forall fun x => (ha.1 x.2).trans_lt hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SupConvergenceClass α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsLUB (range f) a
⊢ Tendsto f atBot (𝓝 a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsGLB (range f) a
⊢ Tendsto f atBot (𝓝 a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddAbove (range f)
⊢ Tendsto f atBot (𝓝 (⨆ i, f i))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderInf α
inst✝ : InfConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddBelow (range f)
⊢ Tendsto f atBot (𝓝 (⨅ i, f i))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderInf α
inst✝ : InfConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ i, f i))

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ (x + y).toENNReal ≤ x.toENNReal + y.toENNReal

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
⊢ SupConvergenceClass (α × β)

Tactic:
by

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

Goal state before:
pp: x z : ℝ
h : ↑x + ⊤ ≤ ↑x + ↑z
⊢ ⊤ ≤ ↑z

Tactic:
by

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

Goal state before:
pp: x : ℝ
x✝ : EReal
h : ↑x + x✝ ≤ ↑x + ⊥
⊢ x✝ ≤ ⊥

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
⊢ SupConvergenceClass ((i : ι) → α i)

Tactic:
by

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

Goal state before:
pp: x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ ↑y ≤ ↑z

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
α : Type u_4
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l)

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
α : Type u_4
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l)

Tactic:
by
  classical
  exact if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
  else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H

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

Goal state before:
pp: x y : EReal
h : x < y
z : ℝ
⊢ ↑z + x < ↑z + y

Tactic:
by

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

Goal state before:
pp: y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + t ≤ y + t

Tactic:
by

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

Goal state before:
pp: x y z t : EReal
h1 : x < y
h2 : z < t
⊢ x + z < y + t

Tactic:
by

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

Goal state before:
pp: x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + t

Tactic:
by

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

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ IsLUB (range f) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
by

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

Goal state before:
pp: x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
by

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

Goal state before:
pp: x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
by

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

Goal state before:
pp: ⊢ (-⊤).toReal = -⊤.toReal

Tactic:
by

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

Goal state before:
pp: ⊢ (-⊥).toReal = -⊥.toReal

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ -a ≤ b ↔ -b ≤ a

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a ≤ -b ↔ b ≤ -a

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x ↦ True) = limsup u f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x ↦ True) = liminf u f

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ -a < b ↔ -b < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x})

Tactic:
by

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

Goal state before:
pp: a b : EReal
⊢ a < -b ↔ b < -a

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)

Tactic:
by

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

Goal state before:
pp: a : EReal
⊢ -a < 0 ↔ 0 < a

Tactic:
by

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

Goal state before:
pp: a : EReal
⊢ -a ≤ 0 ↔ 0 ≤ a

Tactic:
by

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

Goal state before:
pp: a : EReal
⊢ 0 < -a ↔ a < 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_6
α : Type u_7
β : Type u_8
inst✝ : ConditionallyCompleteLattice β
v : ι → α
u : α → β
f : Filter ι
g : Filter α
hv : Tendsto v f g
hvf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (map v f) u
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) g u
⊢ limsup (u ∘ v) f ≤ limsup u g

Tactic:
by

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

Goal state before:
pp: a : EReal
⊢ 0 ≤ -a ↔ a ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ (𝓟 s).limsSup = sSup s

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddAbove (range u)
⊢ limsup u ⊤ = ⨆ i, u i

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ liminf u ⊤ = ⨅ i, u i

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
x : α
hx : u x = v x
⊢ u x ≤ b ↔ v x ∈ {x | (fun n ↦ n ≤ b) x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ 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
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ blimsup u f p = blimsup v f p

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: β : Type u_2
α : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
f : Filter α
inst✝ : f.NeBot
b : β
⊢ limsup (fun x ↦ b) f = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ liminf f v = sSup (⋃ j, ⋂ i, Iic (f ↑i))

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝ : ConditionallyCompleteLattice α
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
i : ι'
hi : p i
h'i : s i = ∅
⊢ liminf f v = sSup univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun i ↦ f (i + k)) atTop = liminf f atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, a ≤ u i
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ a ≤ limsup u f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ⊥ ∈ {a | ∀ᶠ (n : α) in ⊥, n ≤ a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ limsup f ⊥ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ⊤ ∈ {a | ∀ᶠ (n : α) in ⊥, a ≤ n}

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ liminf f ⊥ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, n ≤ a}, ⊤ ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, a ≤ n}, b ≤ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x ↦ False) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x ↦ False) = ⊤

Tactic:
by

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

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊤
h2 : x ≠ ⊤ ∨ y ≠ ⊥
⊢ -(x + y) = -x - y

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ limsup (fun x ↦ ⊥) f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ ⨅ i ∈ f, sSup (u '' id i) = ⨅ s ∈ f, ⨆ a ∈ s, u a

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨅ (_ : True), sSup (u '' Ici i) = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
by

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

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ -(x - y) = -x + y

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ limsup u atTop = ⨅ n, ⨆ i, u (i + n)

Tactic:
by

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
⊢ 0 < -x

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : f.HasBasis p s
⊢ ⨅ i, ⨅ (_ : p i), sSup (u '' s i) = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, u a

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsSup = sSup s

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsInf = sInf s

Tactic:
by

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
H₁ : 0 < -x
⊢ x = -↑(-x).toENNReal

Tactic:
by

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
H₁ : 0 < -x
H₂ : x = -↑(-x).toENNReal
⊢ 0 < (-x).toENNReal

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ limsup u ⊤ = ⨆ i, u i

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ liminf u ⊤ = ⨅ i, u i

Tactic:
by

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
y : EReal
hy : ↑x = y
H₁ : 0 ≤ y
⊢ y.toENNReal = x

Tactic:
by

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
⊢ recENNReal coe neg_coe ↑x = coe x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
I : ι → Ideal R
⊢ emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
by

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

Goal state before:
pp: x : EReal
h : x ≠ ⊥
⊢ x - ⊥ = ⊤

Tactic:
by

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

Goal state before:
pp: x : EReal
hx : x ≠ ⊤
⊢ ⊤ - x = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
⊢ FiniteMultiplicity p.asIdeal (⨆ i, I i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ blimsup u f p = blimsup u f q

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
hf : f.HasBasis p s
q : β → Prop
⊢ blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

Tactic:
by

Goal state after: