awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun (x : ι) ↦ True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : (↑{i : ι | True} : Type u_4) → β
hf : ∀ (i : (↑{i : ι | True} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
⊢ ∃ (f : ι → β), ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩

Premises used: trivial, Subtype.mk, Exists.intro
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun (x : ι) ↦ True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : (↑{i : ι | True} : Type u_4) → β
hf : ∀ (i : (↑{i : ι | True} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
⊢ ∃ (f : ι → β), ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
f : Filter α
inst : ConditionallyCompleteLinearOrder α
a : α
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
h : a < f.limsSup
contrapose! : ∀ (h : ∀ᶠ (x : α) in f, x ≤ a), f.limsSup ≤ a
⊢ ∃ᶠ (n : α) in f, a < n

Tactic:
contrapose! h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
f : Filter α
inst : ConditionallyCompleteLinearOrder α
a : α
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ f.limsSup ≤ a

Tactic:
limsSup_le_of_le hf h

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

Tactic:
exact limsSup_le_of_le hf h

Premises used: Filter.limsSup_le_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
f : Filter α
inst : ConditionallyCompleteLinearOrder α
a : α
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
h : f.limsInf < a
⊢ ∃ᶠ (n : α) in f, n < a

Tactic:
frequently_lt_of_lt_limsSup (α := OrderDual α) hf h

Premises used: Filter.frequently_lt_of_lt_limsSup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
simp_rw : ∃ (c : β), Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c ∧ b < c
⊢ ∃ (c : β) (_ : Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c), b < c

Tactic:
simp_rw [exists_prop]

Premises used: exists_prop
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ ∃ (c : β), Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c ∧ b < c

Tactic:
exists_lt_of_lt_csSup hu h

Premises used: exists_lt_of_lt_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ ∃ (c : β), Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c ∧ b < c

Tactic:
exact exists_lt_of_lt_csSup hu h

Premises used: exists_lt_of_lt_csSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
obtain :
  ∀ (c : β) (hc : Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c) (hbc : b < c),
    ∀ᶠ (a : α) in f, b < u a
⊢ ∀ᶠ (a : α) in f, b < u a

Tactic:
obtain ⟨c, hc, hbc⟩ : ∃ (c : β) (_ : c ∈ { c : β | ∀ᶠ n : α in f, c ≤ u n }), b < c := by
    simp_rw [exists_prop]
    exact exists_lt_of_lt_csSup hu h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
c : β
hc : Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a

Tactic:
hc.mono fun x hx => lt_of_lt_of_le hbc hx

Premises used: Filter.Eventually.mono, lt_of_lt_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
c : β
hc : Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a

Tactic:
exact hc.mono fun x hx => lt_of_lt_of_le hbc hx

Premises used: Filter.Eventually.mono, lt_of_lt_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : limsup u f < b
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
⊢ ∀ᶠ (a : α) in f, u a < b

Tactic:
eventually_lt_of_lt_liminf (β := βᵒᵈ) h hu

Premises used: Filter.eventually_lt_of_lt_liminf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Preorder β
inst_2 : AddZeroClass α
inst_3 : AddLeftStrictMono α
x ε : α
u : β → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
⊢ ∀ᶠ (b : β) in atTop, u b < x + ε

Tactic:
eventually_lt_of_limsup_lt (lt_of_le_of_lt hu (lt_add_of_pos_right x hε)) hu_bdd

Premises used: lt_of_le_of_lt, lt_add_of_pos_right, Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Preorder β
inst_2 : AddZeroClass α
inst_3 : AddLeftStrictMono α
x ε : α
u : β → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
⊢ ∀ᶠ (b : β) in atTop, x + ε < u b

Tactic:
eventually_lt_of_lt_liminf (lt_of_lt_of_le (add_lt_of_neg_right x hε) hu) hu_bdd

Premises used: Filter.eventually_lt_of_lt_liminf, add_lt_of_neg_right, lt_of_lt_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, u n < x + ε

Tactic:
have h : ∀ᶠ n : ℕ in atTop, u n < x + ε := eventually_lt_add_pos_of_limsup_le hu_bdd hu hε
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∀ᶠ (n : ℕ) in atTop, u n < x + ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, u b < x + ε

Tactic:
simp only [eventually_atTop] at h

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∃ (a : ℕ), ∀ b ≥ a, u b < x + ε
obtain : ∀ (n : ℕ) (hn : ∀ b ≥ n, u b < x + ε), ∃ (n : ℕ+), u (↑n : ℕ) < x + ε
⊢ ∃ (n : ℕ+), u (↑n : ℕ) < x + ε

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
n : ℕ
hn : ∀ b ≥ n, u b < x + ε
⊢ ∃ (n : ℕ+), u (↑n : ℕ) < x + ε

Tactic:
⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

Premises used: Nat.le_succ, Subtype.mk, HAdd.hAdd, Nat.succ_pos, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
n : ℕ
hn : ∀ b ≥ n, u b < x + ε
⊢ ∃ (n : ℕ+), u (↑n : ℕ) < x + ε

Tactic:
exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
⊢ ∀ᶠ (n : ℕ) in atTop, x + ε < u n

Tactic:
have h : ∀ᶠ n : ℕ in atTop, x + ε < u n := eventually_add_neg_lt_of_le_liminf hu_bdd hu hε
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∀ᶠ (n : ℕ) in atTop, x + ε < u n
⊢ ∃ (a : ℕ), ∀ b ≥ a, x + ε < u b

Tactic:
simp only [eventually_atTop] at h

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∃ (a : ℕ), ∀ b ≥ a, x + ε < u b
obtain : ∀ (n : ℕ) (hn : ∀ b ≥ n, x + ε < u b), ∃ (n : ℕ+), x + ε < u (↑n : ℕ)
⊢ ∃ (n : ℕ+), x + ε < u (↑n : ℕ)

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
n : ℕ
hn : ∀ b ≥ n, x + ε < u b
⊢ ∃ (n : ℕ+), x + ε < u (↑n : ℕ)

Tactic:
⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

Premises used: Nat.le_succ, Subtype.mk, HAdd.hAdd, Nat.succ_pos, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : AddZeroClass α
inst_2 : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
n : ℕ
hn : ∀ b ≥ n, x + ε < u b
⊢ ∃ (n : ℕ+), x + ε < u (↑n : ℕ)

Tactic:
exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : b < limsup u f
contrapose! : ∀ (h : ∀ᶠ (x : α) in f, u x ≤ b), limsup u f ≤ b
⊢ ∃ᶠ (x : α) in f, b < u x

Tactic:
contrapose! h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ᶠ (x : α) in f, u x ≤ b
apply : ∀ᶠ (n : β) in map u f, n ≤ b
⊢ limsup u f ≤ b

Tactic:
apply limsSup_le_of_le hu

Premises used: Filter.limsSup_le_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ᶠ (x : α) in f, u x ≤ b
⊢ ∀ᶠ (n : β) in map u f, n ≤ b

Tactic:
simpa using h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h : liminf u f < b
⊢ ∃ᶠ (x : α) in f, u x < b

Tactic:
frequently_lt_of_lt_limsup (β := βᵒᵈ) hu h

Premises used: Filter.frequently_lt_of_lt_limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
⊢ limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y

Tactic:
⟨fun h _ h' ↦ eventually_lt_of_limsup_lt (h.trans_lt h') h₂, fun h ↦ ?_⟩

Premises used: Filter.eventually_lt_of_limsup_lt, Iff.intro, LE.le.trans_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
refine : ∀ (h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y), limsup u f ≤ x
⊢ limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y

Tactic:
refine ⟨fun h _ h' ↦ eventually_lt_of_limsup_lt (h.trans_lt h') h₂, fun h ↦ ?_⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
pos : ∀ (h' : ∀ y > x, ∃ (z : β), x < z ∧ z < y), limsup u f ≤ x
neg : ∀ (h' : ¬∀ y > x, ∃ (z : β), x < z ∧ z < y), limsup u f ≤ x
⊢ limsup u f ≤ x

Tactic:
by_cases h' : ∀ y > x, ∃ z, x < z ∧ z < y
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ (z : β), x < z ∧ z < y
pos : ∀ ⦃c : β⦄, x < c → limsup u f < c
⊢ limsup u f ≤ x

Tactic:
rw [← forall_gt_iff_le]

Premises used: forall_gt_iff_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ (z : β), x < z ∧ z < y
y : β
x_y : x < y
pos : ∀ (z : β) (x_z : x < z) (z_y : z < y), limsup u f < y
⊢ limsup u f < y

Tactic:
rcases h' y x_y with ⟨z, x_z, z_y⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ (z : β), x < z ∧ z < y
y : β
x_y : x < y
z : β
x_z : x < z
z_y : z < y
⊢ limsup u f < y

Tactic:
(limsup_le_of_le h₁ ((h z x_z).mono (fun _ ↦ le_of_lt))).trans_lt z_y

Premises used: le_of_lt, Filter.limsup_le_of_le, Filter.Eventually.mono, LE.le.trans_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ (z : β), x < z ∧ z < y
y : β
x_y : x < y
z : β
x_z : x < z
z_y : z < y
⊢ limsup u f < y

Tactic:
exact (limsup_le_of_le h₁ ((h z x_z).mono (fun _ ↦ le_of_lt))).trans_lt z_y

Premises used: le_of_lt, Filter.limsup_le_of_le, Filter.Eventually.mono, LE.le.trans_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ¬∀ y > x, ∃ (z : β), x < z ∧ z < y
neg : ∀ᶠ (n : α) in f, u n ≤ x
⊢ limsup u f ≤ x

Tactic:
apply limsup_le_of_le h₁

Premises used: Filter.limsup_le_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ¬∀ y > x, ∃ (z : β), x < z ∧ z < y
⊢ ∃ y > x, ∀ (z : β), z ≤ x ∨ y ≤ z

Tactic:
push +distrib Not at h'

Premises used: Not
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∃ y > x, ∀ (z : β), z ≤ x ∨ y ≤ z
neg : ∀ (z : β) (x_z : z > x) (hz : ∀ (z_1 : β), z_1 ≤ x ∨ z ≤ z_1), ∀ᶠ (n : α) in f, u n ≤ x
⊢ ∀ᶠ (n : α) in f, u n ≤ x

Tactic:
rcases h' with ⟨z, x_z, hz⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
z : β
x_z : z > x
hz : ∀ (z_1 : β), z_1 ≤ x ∨ z ≤ z_1
⊢ ∀ᶠ (n : α) in f, u n ≤ x

Tactic:
(h z x_z).mono <| fun w hw ↦ (or_iff_left (not_le_of_gt hw)).1 (hz (u w))

Premises used: Filter.Eventually.mono, Iff.mp, or_iff_left, not_le_of_gt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
z : β
x_z : z > x
hz : ∀ (z_1 : β), z_1 ≤ x ∨ z ≤ z_1
⊢ ∀ᶠ (n : α) in f, u n ≤ x

Tactic:
exact (h z x_z).mono <| fun w hw ↦ (or_iff_left (not_le_of_gt hw)).1 (hz (u w))

Premises used: Filter.Eventually.mono, Iff.mp, or_iff_left, not_le_of_gt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
⊢ limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y

Tactic:
⟨fun h _ h' ↦ (eventually_lt_of_limsup_lt (h.trans_lt h') h₂).mono fun _ ↦ le_of_lt, ?_⟩

Premises used: le_of_lt, Filter.eventually_lt_of_limsup_lt, Filter.Eventually.mono, Iff.intro, LE.le.trans_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
refine : (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → limsup u f ≤ x
⊢ limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y

Tactic:
refine ⟨fun h _ h' ↦ (eventually_lt_of_limsup_lt (h.trans_lt h') h₂).mono fun _ ↦ le_of_lt, ?_⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
rw : (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → ∀ ⦃c : β⦄, x < c → limsup u f < c
⊢ (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → limsup u f ≤ x

Tactic:
rw [← forall_gt_iff_le]

Premises used: forall_gt_iff_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y
y : β
x_y : x < y
obtain : ∀ (z : β) (x_z : x < z) (z_y : z < y), limsup u f < y
⊢ limsup u f < y

Tactic:
obtain ⟨z, x_z, z_y⟩ := exists_between x_y

Premises used: exists_between
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y
y : β
x_y : x < y
z : β
x_z : x < z
z_y : z < y
⊢ limsup u f < y

Tactic:
(limsup_le_of_le h₁ (h z x_z)).trans_lt z_y

Premises used: Filter.limsup_le_of_le, LE.le.trans_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y
y : β
x_y : x < y
z : β
x_z : x < z
z_y : z < y
⊢ limsup u f < y

Tactic:
exact (limsup_le_of_le h₁ (h z x_z)).trans_lt z_y

Premises used: Filter.limsup_le_of_le, LE.le.trans_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a

Tactic:
⟨fun h _ h' ↦ frequently_lt_of_lt_limsup h₁ (h'.trans_le h), fun h ↦ ?_⟩

Premises used: LT.lt.trans_le, Iff.intro, Filter.frequently_lt_of_lt_limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
refine : ∀ (h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a), x ≤ limsup u f
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a

Tactic:
refine ⟨fun h _ h' ↦ frequently_lt_of_lt_limsup h₁ (h'.trans_le h), fun h ↦ ?_⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
pos : ∀ (h' : ∀ y < x, ∃ (z : β), y < z ∧ z < x), x ≤ limsup u f
neg : ∀ (h' : ¬∀ y < x, ∃ (z : β), y < z ∧ z < x), x ≤ limsup u f
⊢ x ≤ limsup u f

Tactic:
by_cases h' : ∀ y < x, ∃ z, y < z ∧ z < x
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ (z : β), y < z ∧ z < x
pos : ∀ ⦃c : β⦄, c < x → c < limsup u f
⊢ x ≤ limsup u f

Tactic:
rw [← forall_lt_iff_le]

Premises used: forall_lt_iff_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ (z : β), y < z ∧ z < x
y : β
y_x : y < x
pos : ∀ (z : β) (y_z : y < z) (z_x : z < x), y < limsup u f
⊢ y < limsup u f

Tactic:
obtain ⟨z, y_z, z_x⟩ := h' y y_x
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ (z : β), y < z ∧ z < x
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f

Tactic:
y_z.trans_le (le_limsup_of_frequently_le ((h z z_x).mono (fun _ ↦ le_of_lt)) h₂)

Premises used: Filter.le_limsup_of_frequently_le, le_of_lt, Filter.Frequently.mono, LT.lt.trans_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ (z : β), y < z ∧ z < x
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f

Tactic:
exact y_z.trans_le (le_limsup_of_frequently_le ((h z z_x).mono (fun _ ↦ le_of_lt)) h₂)

Premises used: Filter.le_limsup_of_frequently_le, le_of_lt, Filter.Frequently.mono, LT.lt.trans_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ¬∀ y < x, ∃ (z : β), y < z ∧ z < x
apply : ∃ᶠ (i : α) in f, x ≤ u i
⊢ x ≤ limsup u f

Tactic:
apply le_limsup_of_frequently_le _ h₂

Premises used: Filter.le_limsup_of_frequently_le