awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun (x : β) ↦ True) = liminf u f

Tactic:
simp [bliminf_eq, liminf_eq]

Premises used: Filter.liminf_eq, Filter.bliminf_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup u (f ⊓ 𝓟 {x : β | p x})

Tactic:
simp only [blimsup_eq, limsup_eq, eventually_inf_principal, mem_setOf_eq]

Premises used: Filter.eventually_inf_principal, Filter.blimsup_eq, Set.mem_setOf_eq, Filter.limsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ bliminf u f p = liminf u (f ⊓ 𝓟 {x : β | p x})

Tactic:
blimsup_eq_limsup (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, Filter.blimsup_eq_limsup, setOf, Filter.bliminf, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
rw :
  limsup u (f ⊓ 𝓟 {x : β | p x}) =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
rw₁ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
rw₂ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    (map (α := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
        (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
        (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)).limsSup
rw₃ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    (map u
        (map (α := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
          (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
          (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f))).limsSup
rw₄ rw₅ : (map u (f ⊓ 𝓟 {x : β | p x})).limsSup = (map u (f ⊓ 𝓟 {x : β | p x})).limsSup
⊢ blimsup u f p =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)

Tactic:
rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]

Premises used: Filter.blimsup_eq_limsup, Filter.map_comap_setCoe_val, Filter.map_map, Filter.limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ bliminf u f p =
    liminf (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)

Tactic:
blimsup_eq_limsup_subtype (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.bliminf, Filter.blimsup_eq_limsup_subtype, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : Filter α
a : α
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
h : ∀ᶠ (n : α) in f, n ≤ a
⊢ f.limsSup ≤ a

Tactic:
csInf_le hf h

Premises used: Filter.limsSup, csInf_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : Filter α
a : α
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
h : ∀ᶠ (n : α) in f, a ≤ n
⊢ a ≤ f.limsInf

Tactic:
le_csSup hf h

Premises used: Filter.limsInf, le_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
a : α
hf : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h : ∀ᶠ (n : β) in f, u n ≤ a
⊢ limsup u f ≤ a

Tactic:
csInf_le hf h

Premises used: Filter.limsSup, Filter.limsup, csInf_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
a : α
hf : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h : ∀ᶠ (n : β) in f, a ≤ u n
⊢ a ≤ liminf u f

Tactic:
le_csSup hf h

Premises used: Filter.limsInf, Filter.liminf, le_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : Filter α
a : α
hf : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
h : ∀ (b : α), (∀ᶠ (n : α) in f, n ≤ b) → a ≤ b
⊢ a ≤ f.limsSup

Tactic:
le_csInf hf h

Premises used: Filter.limsSup, le_csInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : Filter α
a : α
hf : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
h : ∀ (b : α), (∀ᶠ (n : α) in f, b ≤ n) → b ≤ a
⊢ f.limsInf ≤ a

Tactic:
csSup_le hf h

Premises used: Filter.limsInf, csSup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
a : α
hf : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h : ∀ (b : α), (∀ᶠ (n : β) in f, u n ≤ b) → a ≤ b
⊢ a ≤ limsup u f

Tactic:
le_csInf hf h

Premises used: Filter.limsSup, le_csInf, Filter.limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
a : α
hf : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h : ∀ (b : α), (∀ᶠ (n : β) in f, b ≤ u n) → b ≤ a
⊢ liminf u f ≤ a

Tactic:
csSup_le hf h

Premises used: Filter.limsInf, Filter.liminf, csSup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : Filter α
inst_1 : f.NeBot
h₁ : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
h₂ : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
⊢ f.limsInf ≤ f.limsSup

Tactic:
liminf_le_of_le h₂ fun a₀ ha₀ =>
    le_limsup_of_le h₁ fun a₁ ha₁ =>
      show a₀ ≤ a₁ from
        let ⟨_, hb₀, hb₁⟩ := (ha₀.and ha₁).exists
        le_trans hb₀ hb₁

Premises used: Filter.liminf, Set.Mem, Filter.map, setOf, Filter.Eventually.and, Filter.le_limsup_of_le, LE.le, Filter.Eventually.exists, _private.0.Filter.limsInf_le_limsSup.match_1, Set.preimage, Filter.liminf_le_of_le, le_trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
inst_1 : f.NeBot
u : β → α
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ limsup u f

Tactic:
limsInf_le_limsSup h h'

Premises used: Filter.limsInf_le_limsSup, Filter.liminf, Filter.limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f g : Filter α
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hg : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) g
h : ∀ (a : α), (∀ᶠ (n : α) in g, n ≤ a) → ∀ᶠ (n : α) in f, n ≤ a
⊢ f.limsSup ≤ g.limsSup

Tactic:
csInf_le_csInf hf hg h

Premises used: Filter.limsSup, csInf_le_csInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f g : Filter α
hf : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
hg : IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) g
h : ∀ (a : α), (∀ᶠ (n : α) in f, a ≤ n) → ∀ᶠ (n : α) in g, a ≤ n
⊢ f.limsInf ≤ g.limsInf

Tactic:
csSup_le_csSup hg hf h

Premises used: Filter.limsInf, csSup_le_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : u ≤ᶠ[f] v
hu : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hv : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ limsup u f ≤ limsup v f

Tactic:
limsSup_le_limsSup hu hv fun _ => h.trans

Premises used: Filter.limsSup_le_limsSup, Filter.limsup, Filter.EventuallyLE.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a ≤ v a
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f v
⊢ liminf u f ≤ liminf v f

Tactic:
limsup_le_limsup (β := βᵒᵈ) h hv hu

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.limsup_le_limsup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f g : Filter α
h : f ≤ g
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hg : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) g
⊢ f.limsSup ≤ g.limsSup

Tactic:
limsSup_le_limsSup hf hg fun _ ha => h ha

Premises used: Filter.limsSup_le_limsSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f g : Filter α
h : g ≤ f
hf : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
hg : IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) g
⊢ f.limsInf ≤ g.limsInf

Tactic:
limsInf_le_limsInf hf hg fun _ ha => h ha

Premises used: Filter.limsInf_le_limsInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : ConditionallyCompleteLattice β
f g : Filter α
h : f ≤ g
u : α → β
hf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) g u
⊢ limsup u f ≤ limsup u g

Tactic:
limsSup_le_limsSup_of_le (map_mono h) hf hg

Premises used: Filter.map_mono, Filter.limsup, Filter.limsSup_le_limsSup_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : 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
rw : limsup u (map v f) ≤ limsup u g
⊢ limsup (u ∘ v) f ≤ limsup u g

Tactic:
rw [limsup_comp]

Premises used: Filter.limsup_comp
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : 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 (map v f) ≤ limsup u g

Tactic:
limsup_le_limsup_of_le hv

Premises used: Filter.limsup_le_limsup_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : 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 (map v f) ≤ limsup u g

Tactic:
exact limsup_le_limsup_of_le hv

Premises used: Filter.limsup_le_limsup_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_6
β : Type u_7
inst : ConditionallyCompleteLattice β
f g : Filter α
h : g ≤ f
u : α → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
hg : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) g u
⊢ liminf u f ≤ liminf u g

Tactic:
limsInf_le_limsInf_of_le (map_mono h) hf hg

Premises used: Filter.map_mono, Filter.limsInf_le_limsInf_of_le, Filter.liminf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
ι : 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
⊢ liminf u g ≤ liminf (u ∘ v) f

Tactic:
hv.limsup_comp_le_limsup (β := βᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.Tendsto.limsup_comp_le_limsup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
simp : sInf {a : α | ∀ x ∈ s, x ≤ a} = sSup s
⊢ (𝓟 s).limsSup = sSup s

Tactic:
simp only [limsSup, eventually_principal]

Premises used: Filter.limsSup, Filter.eventually_principal
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ sInf {a : α | ∀ x ∈ s, x ≤ a} = sSup s

Tactic:
csInf_upperBounds_eq_csSup h hs

Premises used: upperBounds, csInf_upperBounds_eq_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ sInf {a : α | ∀ x ∈ s, x ≤ a} = sSup s

Tactic:
exact csInf_upperBounds_eq_csSup h hs

Premises used: csInf_upperBounds_eq_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
h : BddBelow s
hs : s.Nonempty
⊢ (𝓟 s).limsInf = sInf s

Tactic:
limsSup_principal_eq_csSup (α := αᵒᵈ) h hs

Premises used: Filter.limsInf, setOf, Filter.limsSup_principal_eq_csSup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddAbove (range 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_csSup hu (range_nonempty _), sSup_range]

Premises used: Filter.map_top, Filter.limsup, Filter.limsSup_principal_eq_csSup, Set.range_nonempty, sSup_range
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddBelow (range 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_csSup hu (range_nonempty _), sInf_range]

Premises used: Filter.liminf, Filter.map_top, Set.range_nonempty, sInf_range, Filter.limsInf_principal_eq_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
rw : sInf {a : β | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
⊢ limsup u f = limsup v f

Tactic:
rw [limsup_eq]

Premises used: Filter.limsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
e_a : ∀ (b : β), (∀ᶠ (n : α) in f, u n ≤ b) ↔ ∀ᶠ (n : β) in map v f, n ≤ b
⊢ sInf {a : β | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f

Tactic:
congr with b
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : 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 ↔ Membership.mem (γ := Set β) {x : β | (fun (n : β) ↦ n ≤ b) x} (v x)

Tactic:
simp [hx]
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ (∀ᶠ (n : α) in f, u n ≤ b) ↔ ∀ᶠ (n : β) in map v f, n ≤ b

Tactic:
exact eventually_congr (h.mono fun x hx => by simp [hx])

Premises used: Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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:
simpa only [blimsup_eq_limsup] using limsup_congr <| eventually_inf_principal.2 h

Premises used: Filter.eventually_inf_principal, Iff.mpr, Filter.blimsup_eq_limsup, Filter.limsup_congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ bliminf u f p = bliminf v f p

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

Premises used: setOf, Filter.bliminf, OrderDual, Filter.blimsup_congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ liminf u f = liminf v f

Tactic:
limsup_congr (β := βᵒᵈ) h

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.limsup_congr, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
inst_1 : f.NeBot
b : β
⊢ limsup (fun (x : α) ↦ b) f = b

Tactic:
simpa only [limsup_eq, eventually_const] using csInf_Ici

Premises used: Filter.eventually_const, csInf_Ici, Filter.limsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
inst_1 : f.NeBot
b : β
⊢ liminf (fun (x : α) ↦ b) f = b

Tactic:
limsup_const (β := βᵒᵈ) b

Premises used: Filter.limsInf, Filter.limsup_const, Filter.liminf, setOf, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
simp_rw :
  Eq.{u_1 + 1} (α := α) (sSup {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x})
    (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι))))
⊢ liminf f v = sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι)))

Tactic:
simp_rw [liminf_eq, hv.eventually_iff]

Premises used: Filter.liminf_eq, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
e_a :
  Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x}
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι)))
⊢ Eq.{u_1 + 1} (α := α) (sSup {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x})
    (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι))))

Tactic:
congr 1
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
e_a :
  ∀ (x : α),
    Membership.mem (γ := Set α) {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} x ↔
      Membership.mem (γ := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι))) x
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x}
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι)))

Tactic:
ext x
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
x : α
⊢ Membership.mem (γ := Set α) {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} x ↔
    Membership.mem (γ := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι))) x

Tactic:
simp only [mem_setOf_eq, iInter_coe_set, mem_iUnion, mem_iInter, mem_Iic, Subtype.exists,
    exists_prop]

Premises used: Set.mem_iUnion, Subtype.exists, Set.mem_setOf_eq, exists_prop, Set.mem_iInter, Set.mem_Iic, Set.iInter_coe_set
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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:
simp [hv.eq_bot_iff.2 ⟨i, hi, h'i⟩, liminf_eq]

Premises used: Filter.liminf_eq, Iff.mpr, Filter.HasBasis.eq_bot_iff, And.intro, Exists.intro
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ limsup f v = sInf (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Ici (f (↑i : ι)))

Tactic:
HasBasis.liminf_eq_sSup_iUnion_iInter (α := αᵒᵈ) hv

Premises used: Filter.limsSup, Set.Ici, setOf, Filter.limsup, Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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 = ∅
⊢ limsup f v = sInf univ

Tactic:
HasBasis.liminf_eq_sSup_univ_of_empty (α := αᵒᵈ) hv i hi h'i

Premises used: Filter.limsSup, setOf, Filter.limsup, Filter.HasBasis.liminf_eq_sSup_univ_of_empty, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
rw : liminf (β := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop = liminf f atTop
rw₁ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = liminf f atTop
rw₂ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = (map f atTop).limsInf
rw₃ : (map f (map (fun (i : ℕ) ↦ i + k) atTop)).limsInf = (map f atTop).limsInf
rw₄ rw₅ : (map f atTop).limsInf = (map f atTop).limsInf
⊢ liminf (fun (i : ℕ) ↦ f (i + k)) atTop = liminf f atTop

Tactic:
rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]

Premises used: Filter.liminf, Filter.map_map, Function.comp_def, Filter.map_add_atTop_eq_nat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ limsup (fun (i : ℕ) ↦ f (i + k)) atTop = limsup f atTop

Tactic:
@liminf_nat_add αᵒᵈ _ f k

Premises used: Filter.limsSup, setOf, Filter.limsup, Filter.liminf_nat_add, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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:
le_limsup_of_le hu_le fun b hb ↦ ?_

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

Tactic:
refine le_limsup_of_le hu_le fun b hb ↦ ?_

Premises used: Filter.le_limsup_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : 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
b : α
hb : ∀ᶠ (n : ι) in f, u n ≤ b
obtain : ∀ (n : ι) (han : a ≤ u n) (hnb : u n ≤ b), a ≤ b
⊢ a ≤ b

Tactic:
obtain ⟨n, han, hnb⟩ := (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, a ≤ u i
hu_le : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, u n ≤ b
n : ι
han : a ≤ u n
hnb : u n ≤ b
⊢ a ≤ b

Tactic:
han.trans hnb

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, a ≤ u i
hu_le : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, u n ≤ b
n : ι
han : a ≤ u n
hnb : u n ≤ b
⊢ a ≤ b

Tactic:
exact han.trans hnb

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
⊢ liminf u f ≤ a

Tactic:
liminf_le_of_le hu_le fun b hb ↦ ?_

Premises used: Filter.liminf_le_of_le
-- 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
refine : ∀ (b : α) (hb : ∀ᶠ (n : ι) in f, b ≤ u n), b ≤ a
⊢ liminf u f ≤ a

Tactic:
refine liminf_le_of_le hu_le fun b hb ↦ ?_

Premises used: Filter.liminf_le_of_le