awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
obtain : ∀ (n : ι) (hna : u n ≤ a) (hbn : b ≤ u n), b ≤ a
⊢ b ≤ a

Tactic:
obtain ⟨n, hna, hbn⟩ := (hu.and_eventually hb).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
n : ι
hna : u n ≤ a
hbn : b ≤ u n
⊢ b ≤ a

Tactic:
hbn.trans hna

Premises used: LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
n : ι
hna : u n ≤ a
hbn : b ≤ u n
⊢ b ≤ a

Tactic:
exact hbn.trans hna

Premises used: LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ Membership.mem (γ := Set α) {a : α | ∀ᶠ (n : α) in ⊥, n ≤ a} ⊥

Tactic:
simp
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
⊢ limsup f ⊥ = ⊥

Tactic:
simp [limsup]

Premises used: Filter.limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ Membership.mem (γ := Set α) {a : α | ∀ᶠ (n : α) in ⊥, a ≤ n} ⊤

Tactic:
simp
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
⊢ liminf f ⊥ = ⊤

Tactic:
simp [liminf]

Premises used: Filter.liminf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ ∀ (b : α), Membership.mem (γ := Set α) {a : α | ∀ᶠ (n : α) in ⊤, n ≤ a} b → ⊤ ≤ b

Tactic:
simpa [eq_univ_iff_forall] using fun b hb => top_unique <| hb _

Premises used: Set.eq_univ_iff_forall, top_unique
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ ∀ (b : α), Membership.mem (γ := Set α) {a : α | ∀ᶠ (n : α) in ⊤, a ≤ n} b → b ≤ ⊥

Tactic:
simpa [eq_univ_iff_forall] using fun b hb => bot_unique <| hb _

Premises used: Set.eq_univ_iff_forall, bot_unique
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun (x : β) ↦ False) = ⊥

Tactic:
simp [blimsup_eq]

Premises used: Filter.blimsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun (x : β) ↦ False) = ⊤

Tactic:
simp [bliminf_eq]

Premises used: Filter.bliminf_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
rw : LE.le.{u_1} (α := α) (sInf {a : α | ∀ᶠ (n : β) in f, ⊥ ≤ a}) ⊥
⊢ Eq.{u_1 + 1} (α := α) (limsup (fun (x : β) ↦ ⊥) f) ⊥

Tactic:
rw [limsup_eq, eq_bot_iff]

Premises used: eq_bot_iff, Filter.limsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
⊢ LE.le.{u_1} (α := α) (sInf {a : α | ∀ᶠ (n : β) in f, ⊥ ≤ a}) ⊥

Tactic:
sInf_le (Eventually.of_forall fun _ => le_rfl)

Premises used: le_rfl, Filter.Eventually.of_forall, sInf_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
⊢ LE.le.{u_1} (α := α) (sInf {a : α | ∀ᶠ (n : β) in f, ⊥ ≤ a}) ⊥

Tactic:
exact sInf_le (Eventually.of_forall fun _ => le_rfl)

Premises used: le_rfl, Filter.Eventually.of_forall, sInf_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
⊢ Eq.{u_1 + 1} (α := α) (liminf (fun (x : β) ↦ ⊤) f) ⊤

Tactic:
limsup_const_bot (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.limsup_const_bot, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_6
p : ι → Prop
s : ι → Set α
f : Filter α
h : f.HasBasis p s
⊢ f.limsSup = ⨅ (i : ι), ⨅ (_ : p i), sSup (s i)

Tactic:
le_antisymm (le_iInf₂ fun i hi => sInf_le <| h.eventually_iff.2 ⟨i, hi, fun _ => le_sSup⟩)
    (le_sInf fun _ ha =>
      let ⟨_, hi, ha⟩ := h.eventually_iff.1 ha
      iInf₂_le_of_le _ hi <| sSup_le ha)

Premises used: Iff.mpr, iInf, iInf₂_le_of_le, _private.0.Filter.HasBasis.limsSup_eq_iInf_sSup.match_1, LE.le, le_iInf₂, le_antisymm, sInf_le, And.intro, Exists.intro, Iff.mp, Filter.HasBasis.eventually_iff, le_sInf, le_sSup, sSup_le, SupSet.sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
p : ι → Prop
s : ι → Set α
f : Filter α
h : f.HasBasis p s
⊢ f.limsInf = ⨆ (i : ι), ⨆ (_ : p i), sInf (s i)

Tactic:
HasBasis.limsSup_eq_iInf_sSup (α := αᵒᵈ) h

Premises used: Filter.limsInf, iSup, setOf, OrderDual, Filter.HasBasis.limsSup_eq_iInf_sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : Filter α
⊢ f.limsSup = ⨅ s ∈ f, sSup s

Tactic:
f.basis_sets.limsSup_eq_iInf_sSup

Premises used: Filter.basis_sets, Filter.HasBasis.limsSup_eq_iInf_sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : Filter α
⊢ f.limsInf = ⨆ s ∈ f, sInf s

Tactic:
limsSup_eq_iInf_sSup (α := αᵒᵈ)

Premises used: Filter.limsInf, Set.Mem, iSup, setOf, Filter.limsSup_eq_iInf_sSup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
isBoundedDefault
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
isBoundedDefault
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
u : β → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, sSup (u '' id i)) (⨅ s ∈ f, ⨆ a ∈ s, u a)

Tactic:
simp only [sSup_image, id]

Premises used: id, sSup_image
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
simp : Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ a ∈ Ici i, u a) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : True), sSup (u '' Ici i)) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)

Tactic:
simp only [sSup_image, iInf_const]

Premises used: sSup_image, iInf_const
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ a ∈ Ici i, u a) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)

Tactic:
rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ limsup u atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), u (i + n)

Tactic:
simp only [limsup_eq_iInf_iSup_of_nat, iSup_ge_eq_iSup_nat_add]

Premises used: iSup_ge_eq_iSup_nat_add, Filter.limsup_eq_iInf_iSup_of_nat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : f.HasBasis p s
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ι), ⨅ (_ : p i), sSup (u '' s i)) (⨅ (i : ι), ⨅ (_ : p i), ⨆ a ∈ s i, u a)

Tactic:
simp only [sSup_image]

Premises used: sSup_image
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsSup = sSup s

Tactic:
simpa only [limsSup, eventually_principal] using sInf_upperBounds_eq_sSup s

Premises used: Filter.limsSup, Filter.eventually_principal, sInf_upperBounds_eq_sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsInf = sInf s

Tactic:
simpa only [limsInf, eventually_principal] using sSup_lowerBounds_eq_sInf s

Premises used: Filter.limsInf, sSup_lowerBounds_eq_sInf, Filter.eventually_principal
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsSup = ⨆ (i : β), u i
rw₁ : (𝓟 (range u)).limsSup = ⨆ (i : β), u i
rw₂ : sSup (range u) = ⨆ (i : β), u i
rw₃ rw₄ : iSup u = ⨆ (i : β), u i
⊢ limsup u ⊤ = ⨆ (i : β), u i

Tactic:
rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]

Premises used: Filter.map_top, Filter.limsup, Filter.limsSup_principal_eq_sSup, sSup_range
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsInf = ⨅ (i : β), u i
rw₁ : (𝓟 (range u)).limsInf = ⨅ (i : β), u i
rw₂ : sInf (range u) = ⨅ (i : β), u i
rw₃ rw₄ : iInf u = ⨅ (i : β), u i
⊢ liminf u ⊤ = ⨅ (i : β), u i

Tactic:
rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]

Premises used: Filter.liminf, Filter.map_top, Filter.limsInf_principal_eq_sInf, sInf_range
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
simp :
  Eq.{u_1 + 1} (α := α) (sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}) (sInf {a : α | ∀ᶠ (x : β) in f, q x → u x ≤ a})
⊢ blimsup u f p = blimsup u f q

Tactic:
simp only [blimsup_eq]

Premises used: Filter.blimsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
e_a : ∀ (a : α), (∀ᶠ (x : β) in f, p x → u x ≤ a) ↔ ∀ᶠ (x : β) in f, q x → u x ≤ a
⊢ Eq.{u_1 + 1} (α := α) (sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}) (sInf {a : α | ∀ᶠ (x : β) in f, q x → u x ≤ a})

Tactic:
congr with a
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
⊢ (∀ᶠ (x : β) in f, p x → u x ≤ a) ↔ ∀ᶠ (x : β) in f, q x → u x ≤ a

Tactic:
eventually_congr (h.mono fun b hb => ?_)

Premises used: Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
e_a : ∀ (b : β) (hb : u b ≠ ⊥ → (p b ↔ q b)), p b → u b ≤ a ↔ q b → u b ≤ a
⊢ (∀ᶠ (x : β) in f, p x → u x ≤ a) ↔ ∀ᶠ (x : β) in f, q x → u x ≤ a

Tactic:
refine eventually_congr (h.mono fun b hb => ?_)

Premises used: Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
e_a : ∀ (hu : u b = ⊥), p b → u b ≤ a ↔ q b → u b ≤ a
e_a₁ : ∀ (hu : u b ≠ ⊥), p b → u b ≤ a ↔ q b → u b ≤ a
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
rcases eq_or_ne (u b) ⊥ with hu | hu

Premises used: Bot.bot, eq_or_ne
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
simp [hu]
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
e_a e_a₁ : q b → u b ≤ a ↔ q b → u b ≤ a
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
rw [hb hu]
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊤ → (p x ↔ q x)
⊢ bliminf u f p = bliminf u f q

Tactic:
blimsup_congr' (α := αᵒᵈ) h

Premises used: setOf, Filter.bliminf, Filter.blimsup_congr', OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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:
simp only [blimsup_eq_limsup, (hf.inf_principal _).limsup_eq_iInf_iSup, mem_inter_iff, iSup_and,
    mem_setOf_eq]

Premises used: Filter.blimsup_eq_limsup, Set.mem_inter_iff, Set.mem_setOf_eq, Filter.HasBasis.inf_principal, Filter.HasBasis.limsup_eq_iInf_iSup, iSup_and
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ blimsup u f p = ⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b

Tactic:
simp only [f.basis_sets.blimsup_eq_iInf_iSup, iSup_and', id, and_comm]

Premises used: iSup_and', id, and_comm, Filter.basis_sets, Filter.HasBasis.blimsup_eq_iInf_iSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ blimsup u atTop p = ⨅ (i : ℕ), ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), u j

Tactic:
simp only [atTop_basis.blimsup_eq_iInf_iSup, @and_comm (p _), iSup_and, mem_Ici, iInf_true]

Premises used: Filter.atTop_basis, and_comm, Set.mem_Ici, Filter.HasBasis.blimsup_eq_iInf_iSup, iSup_and, iInf_true
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
u : β → α
⊢ liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a

Tactic:
limsup_eq_iInf_iSup (α := αᵒᵈ)

Premises used: Filter.limsInf, iInf, Filter.liminf, iSup, setOf, Filter.limsup_eq_iInf_iSup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ liminf u atTop = ⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), u i

Tactic:
@limsup_eq_iInf_iSup_of_nat αᵒᵈ _ u

Premises used: Filter.limsInf, iInf, Filter.liminf, iSup, setOf, OrderDual, Filter.limsup_eq_iInf_iSup_of_nat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ liminf u atTop = ⨆ (n : ℕ), ⨅ (i : ℕ), u (i + n)

Tactic:
@limsup_eq_iInf_iSup_of_nat' αᵒᵈ _ _

Premises used: Filter.limsInf, iInf, Filter.liminf, iSup, setOf, Filter.limsup_eq_iInf_iSup_of_nat', OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : f.HasBasis p s
⊢ liminf u f = ⨆ (i : ι), ⨆ (_ : p i), ⨅ a ∈ s i, u a

Tactic:
HasBasis.limsup_eq_iInf_iSup (α := αᵒᵈ) h

Premises used: Filter.limsInf, iInf, Filter.liminf, iSup, setOf, OrderDual, Filter.HasBasis.limsup_eq_iInf_iSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ bliminf u f p = ⨆ s ∈ f, ⨅ (b : β), ⨅ (_ : p b ∧ b ∈ s), u b

Tactic:
@blimsup_eq_iInf_biSup αᵒᵈ β _ f p u

Premises used: iInf, iSup, setOf, Filter.bliminf, Filter.blimsup_eq_iInf_biSup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ bliminf u atTop p = ⨆ (i : ℕ), ⨅ (j : ℕ), ⨅ (_ : p j ∧ i ≤ j), u j

Tactic:
@blimsup_eq_iInf_biSup_of_nat αᵒᵈ _ p u

Premises used: iInf, iSup, setOf, Filter.bliminf, OrderDual, Filter.blimsup_eq_iInf_biSup_of_nat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : CompleteLattice α
f : Filter β
u : ι → β → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), liminf (u i) f) (liminf (fun (b : β) ↦ ⨆ (i : ι), u i b) f)

Tactic:
iSup_le fun i ↦ liminf_le_liminf <| .of_forall fun b ↦ le_iSup (u · b) i

Premises used: le_iSup, Filter.Eventually.of_forall, Filter.liminf_le_liminf, iSup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : CompleteLattice α
f : Filter β
u : ι → β → α
⊢ LE.le.{u_1} (α := α) (limsup (fun (b : β) ↦ ⨅ (i : ι), u i b) f) (⨅ (i : ι), limsup (u i) f)

Tactic:
iSup_liminf_le_liminf_iSup (α := αᵒᵈ)

Premises used: Filter.limsSup, iInf, setOf, Filter.limsup, Filter.iSup_liminf_le_liminf_iSup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
a₁ : limsup a F ≤ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)
a₂ : sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F
⊢ limsup a F = sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
a₁ :
  LE.le.{u_7} (α := R) (sInf {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1})
    (sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets))
⊢ limsup a F ≤ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)

Tactic:
rw [limsup_eq]

Premises used: Filter.limsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
⊢ LE.le.{u_7} (α := R) (sInf {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1})
    (sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets))

Tactic:
sInf_le_sInf fun x hx => ?_

Premises used: sInf_le_sInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
a₁ :
  ∀ (x : R) (hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x),
    Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x
⊢ LE.le.{u_7} (α := R) (sInf {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1})
    (sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets))

Tactic:
refine sInf_le_sInf fun x hx => ?_

Premises used: sInf_le_sInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
x : R
hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x
a₁ :
  ∀ (I : Set ι) (I_mem_F : I ∈ F.sets) (hI : sSup (a '' I) = x),
    Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x
⊢ Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x

Tactic:
rcases (mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩

Premises used: Set.mem_image, Filter.sets, Iff.mp
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
x : R
hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
h : ∀ (i : ι) (hi : i ∈ I), a i ≤ x
⊢ Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x

Tactic:
filter_upwards [I_mem_F] with i hi
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
x : R
hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x

Tactic:
hI ▸ le_sSup (mem_image_of_mem _ hi)

Premises used: Eq.rec, Set.mem_image_of_mem, le_sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
x : R
hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x

Tactic:
exact hI ▸ le_sSup (mem_image_of_mem _ hi)
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
⊢ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_

Premises used: Filter.limsSup, Filter.limsup, Set.mem_image_of_mem, le_sInf, Set.image, sInf_le_of_le, sSup_le, SupSet.sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
a₁ :
  ∀ (b : R) (hb : Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : R) in map a F, n ≤ a_1} b),
    ∀ b_1 ∈ a '' a ⁻¹' {x : R | (fun (n : R) ↦ n ≤ b) x}, b_1 ≤ b
⊢ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_

Premises used: Set.mem_image_of_mem, le_sInf, sInf_le_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
b : R
hb : Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : R) in map a F, n ≤ a_1} b
w : ι
h : w ∈ a ⁻¹' {x : R | (fun (n : R) ↦ n ≤ b) x}
⊢ a w ≤ b

Tactic:
h

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
b : R
hb : Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : R) in map a F, n ≤ a_1} b
w : ι
h : w ∈ a ⁻¹' {x : R | (fun (n : R) ↦ n ≤ b) x}
⊢ a w ≤ b

Tactic:
exact h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
⊢ liminf a F = sSup ((fun (I : Set ι) ↦ sInf (a '' I)) '' F.sets)

Tactic:
@Filter.limsup_eq_sInf_sSup ι (OrderDual R) _ _ a

Premises used: Filter.limsInf, Filter.liminf, setOf, OrderDual, Filter.limsup_eq_sInf_sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
rw : sSup {a : β | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
⊢ liminf u f ≤ x

Tactic:
rw [liminf_eq]

Premises used: Filter.liminf_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a : β | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x

Tactic:
sSup_le fun b hb => ?_

Premises used: sSup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
refine : ∀ (b : β) (hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b), b ≤ x
⊢ sSup {a : β | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x

Tactic:
refine sSup_le fun b hb => ?_

Premises used: sSup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
contrapose! : ∀ (h : ∀ᶠ (x_1 : α) in f, ¬b ≤ x), ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x

Tactic:
contrapose! h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
h : ∀ᶠ (x_1 : α) in f, ¬b ≤ x
⊢ ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x

Tactic:
hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
h : ∀ᶠ (x_1 : α) in f, ¬b ≤ x
⊢ ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x

Tactic:
exact hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x

Tactic:
have hbx : ∃ᶠ _ in f, b ≤ x := by
    contrapose! h
    exact hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
⊢ b ≤ x

Tactic:
hbx.exists.choose_spec

Premises used: Exists.choose_spec, Filter.Frequently.exists
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
⊢ b ≤ x

Tactic:
exact hbx.exists.choose_spec

Premises used: Exists.choose_spec, Filter.Frequently.exists
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, x ≤ u a
⊢ x ≤ limsup u f

Tactic:
liminf_le_of_frequently_le' (β := βᵒᵈ) h

Premises used: Filter.limsSup, setOf, Filter.liminf_le_of_frequently_le', Filter.limsup, OrderDual