awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
simp_rw : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, aᶜ ⊓ ⨆ a ∈ i, u a) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
⊢ Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
have simp_rw₁ : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, ⨆ i_1 ∈ i, aᶜ ⊓ u i_1) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
Tactic: simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
⊢ a \ limsup u f = liminf (fun (b : β) ↦ a \ u b) f
have rw : (a \ limsup u f)ᶜ = (liminf (fun (b : β) ↦ a \ u b) f)ᶜ
Tactic: rw [← compl_inj_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun (b : β) ↦ a \ u b) f
have rw : (a \ liminf u f)ᶜ = (limsup (fun (b : β) ↦ a \ u b) f)ᶜ
Tactic: rw [← compl_inj_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ blimsup s cofinite p = {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
have simp : Eq.{u_1 + 1} (α := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}})
  {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
Tactic: simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}})
    {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x ↔
    Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x ↔
    Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
have h : ∀ (h : Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x),
  Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
Tactic: refine ⟨fun h => ?_, fun hx t h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h :
  ∀ (h : Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x),
    Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
⊢ Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x ↔
    Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
have h₁ : ∀ (hx : Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x) (t : Set α)
  (h : Membership.mem (γ := Set (Set α)) {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}} t), x ∈ t
Tactic: refine ⟨fun h => ?_, fun hx t h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x
⊢ Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
have h₁ : ∀ (h : x ∉ {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}),
  x ∉ ⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
t : Set α
h : Membership.mem (γ := Set (Set α)) {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}} t
⊢ x ∈ t
have h₁ : ∀ (h : x ∉ t), t ∉ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
⊢ x ∉ ⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}
have h₁ : ∃ (x_1 : Set α), Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ x_1} ∧ x ∉ x_1
Tactic: simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}
have rw : (bliminf s cofinite p)ᶜ = {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}ᶜ
Tactic: rw [← compl_inj_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ (bliminf s cofinite p)ᶜ = {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}ᶜ
have simp : Eq.{u_1 + 1} (α := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ (s n)ᶜ}}
  {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}ᶜ
Tactic: simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup,
    cofinite.blimsup_set_eq]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
have hx₁ : Membership.mem (γ := Set α) (⨅ s ∈ l, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b) x
Tactic: rw [blimsup_eq_iInf_biSup] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : Membership.mem (γ := Set α) (⨅ s ∈ l, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b) x
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
have hx₁ : ∀ (i : Set β) (i_1 : i ∈ l), ∃ (i_2 : β), (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
Tactic: simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ (i : Set β) (i_1 : i ∈ l), ∃ (i_2 : β), (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
have choose : ∀ (g : (i : Set β) → (i : i ∈ l) → β) (hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i)
  (hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)),
  ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
Tactic: choose g hg hg' using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
have refine_1 : ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) sorry) i)
Tactic: refine ⟨fun i : { i | q i } => g (b i) (hl.mem_of_mem i.2), fun i => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
refine_1 : ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i)
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
have refine_2 : ∀ (i : (↑{i : ι | q i} : Type u_4)),
  p ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) sorry) i) ∧
    (fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) sorry) i ∈ b (↑i : ι)
Tactic: refine ⟨fun i : { i | q i } => g (b i) (hl.mem_of_mem i.2), fun i => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
have obtain : ∀ (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: obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
f : Filter α
inst : ConditionallyCompleteLinearOrder α
a : α
hf : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
h : a < f.limsSup
⊢ ∃ᶠ (n : α) in f, a < n
have contrapose! : ∀ (h : ∀ᶠ (x : α) in f, x ≤ a), f.limsSup ≤ a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
have simp_rw : ∃ (c : β), Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c ∧ b < c
Tactic: simp_rw [exists_prop]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ᶠ (a : α) in f, b < u a
have obtain : ∀ (c : β) (hc : Membership.mem (γ := Set β) {c : β | ∀ᶠ (n : α) in f, c ≤ u n} c) (hbc : b < c),
  ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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 : ℕ+), u (↑n : ℕ) < x + ε
have h : ∀ᶠ (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ε
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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 + ε
⊢ ∃ (n : ℕ+), u (↑n : ℕ) < x + ε
have h₁ : ∃ (a : ℕ), ∀ b ≥ a, u b < x + ε
Tactic: simp only [eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 + ε
⊢ ∃ (n : ℕ+), u (↑n : ℕ) < x + ε
have obtain : ∀ (n : ℕ) (hn : ∀ b ≥ n, u b < x + ε), ∃ (n : ℕ+), u (↑n : ℕ) < x + ε
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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 : ℕ+), x + ε < u (↑n : ℕ)
have h : ∀ᶠ (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ε
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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
⊢ ∃ (n : ℕ+), x + ε < u (↑n : ℕ)
have h₁ : ∃ (a : ℕ), ∀ b ≥ a, x + ε < u b
Tactic: simp only [eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∃ (n : ℕ+), x + ε < u (↑n : ℕ)
have obtain : ∀ (n : ℕ) (hn : ∀ b ≥ n, x + ε < u b), ∃ (n : ℕ+), x + ε < u (↑n : ℕ)
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∃ᶠ (x : α) in f, b < u x
have contrapose! : ∀ (h : ∀ᶠ (x : α) in f, u x ≤ b), limsup u f ≤ b
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ limsup u f ≤ b
have apply : ∀ᶠ (n : β) in map u f, n ≤ b
Tactic: apply limsSup_le_of_le hu
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
have refine : ∀ (h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y), limsup u f ≤ x
Tactic: refine ⟨fun h _ h' ↦ eventually_lt_of_limsup_lt (h.trans_lt h') h₂, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ limsup u f ≤ x
have pos : ∀ (h' : ∀ y > x, ∃ (z : β), x < z ∧ z < y), limsup u f ≤ x
Tactic: by_cases h' : ∀ y > x, ∃ z, x < z ∧ z < y
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ limsup u f ≤ x
have neg : ∀ (h' : ¬∀ y > x, ∃ (z : β), x < z ∧ z < y), limsup u f ≤ x
Tactic: by_cases h' : ∀ y > x, ∃ z, x < z ∧ z < y
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ limsup u f ≤ x
have pos : ∀ ⦃c : β⦄, x < c → limsup u f < c
Tactic: rw [← forall_gt_iff_le]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ limsup u f < y
have pos : ∀ (z : β) (x_z : x < z) (z_y : z < y), limsup u f < y
Tactic: rcases h' y x_y with ⟨z, x_z, z_y⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ limsup u f ≤ x
have neg : ∀ᶠ (n : α) in f, u n ≤ x
Tactic: apply limsup_le_of_le h₁
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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
⊢ ∀ᶠ (n : α) in f, u n ≤ x
have h'₁ : ∃ y > x, ∀ (z : β), z ≤ x ∨ y ≤ z
Tactic: push +distrib Not at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ᶠ (n : α) in f, u n ≤ x
have neg : ∀ (z : β) (x_z : z > x) (hz : ∀ (z_1 : β), z_1 ≤ x ∨ z ≤ z_1), ∀ᶠ (n : α) in f, u n ≤ x
Tactic: rcases h' with ⟨z, x_z, hz⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
have refine : (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → limsup u f ≤ x
Tactic: refine ⟨fun h _ h' ↦ (eventually_lt_of_limsup_lt (h.trans_lt h') h₂).mono fun _ ↦ le_of_lt, ?_⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → limsup u f ≤ x
have rw : (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → ∀ ⦃c : β⦄, x < c → limsup u f < c
Tactic: rw [← forall_gt_iff_le]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ limsup u f < y
have obtain : ∀ (z : β) (x_z : x < z) (z_y : z < y), limsup u f < y
Tactic: obtain ⟨z, x_z, z_y⟩ := exists_between x_y
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
have refine : ∀ (h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a), x ≤ limsup u f
Tactic: refine ⟨fun h _ h' ↦ frequently_lt_of_lt_limsup h₁ (h'.trans_le h), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ x ≤ limsup u f
have pos : ∀ (h' : ∀ y < x, ∃ (z : β), y < z ∧ z < x), x ≤ limsup u f
Tactic: by_cases h' : ∀ y < x, ∃ z, y < z ∧ z < x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ x ≤ limsup u f
have neg : ∀ (h' : ¬∀ y < x, ∃ (z : β), y < z ∧ z < x), x ≤ limsup u f
Tactic: by_cases h' : ∀ y < x, ∃ z, y < z ∧ z < x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ x ≤ limsup u f
have pos : ∀ ⦃c : β⦄, c < x → c < limsup u f
Tactic: rw [← forall_lt_iff_le]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ y < limsup u f
have pos : ∀ (z : β) (y_z : y < z) (z_x : z < x), y < limsup u f
Tactic: obtain ⟨z, y_z, z_x⟩ := h' y y_x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ x ≤ limsup u f
have apply : ∃ᶠ (i : α) in f, x ≤ u i
Tactic: apply le_limsup_of_frequently_le _ h₂
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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
⊢ ∃ᶠ (i : α) in f, x ≤ u i
have h'₁ : ∃ y < x, ∀ (z : β), z ≤ y ∨ x ≤ z
Tactic: push +distrib Not at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : β), z ≤ y ∨ x ≤ z
⊢ ∃ᶠ (i : α) in f, x ≤ u i
have rcases : ∀ (z : β) (z_x : z < x) (hz : ∀ (z_1 : β), z_1 ≤ z ∨ x ≤ z_1), ∃ᶠ (i : α) in f, x ≤ u i
Tactic: rcases h' with ⟨z, z_x, hz⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
have refine : (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → x ≤ limsup u f
Tactic: refine ⟨fun h _ h' ↦ (frequently_lt_of_lt_limsup h₁ (h'.trans_le h)).mono fun _ ↦ le_of_lt, ?_⟩