awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
pos : ∀ (h : (Set.Ioo c b).Nonempty), h.some (s := Set.Ioo c b) < b
⊢ (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c) < b
have neg : ∀ (h : ¬(Set.Ioo c b).Nonempty), c < b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
have hb'b : b' < b
Tactic: have hb'b : b' < b := by
    simp only [b']
    split_ifs with h
    exacts [h.some_mem.2, hb]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
⊢ ∀ᶠ (r : α) in atTop,
    LE.le.{u_8} (α := β) (limsup (fun (x : ι) ↦ u x r) cofinite)
      (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c)
have pos : ∀ (h : (Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
pos :
  ∀ (h : (Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)
⊢ ∀ᶠ (r : α) in atTop,
    LE.le.{u_8} (α := β) (limsup (fun (x : ι) ↦ u x r) cofinite)
      (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c)
have neg : ∀ (h : ¬(Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : (Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (b_1 : α) ↦ limsup (fun (i : ι) ↦ u i b_1) cofinite < h.some (s := Set.Ioo c b)) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (r : α) ↦ limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)) x} x}
    a
Tactic: filter_upwards [(tendsto_order.1 h_limsup).2 _ h.some_mem.1] with r hr using hr.le
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : (Set.Ioo c b).Nonempty
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (b_1 : α) ↦ limsup (fun (i : ι) ↦ u i b_1) cofinite < h.some (s := Set.Ioo c b)) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (r : α) ↦ limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)) x} x}
      a
⊢ ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)
have h₂ : ∀ (a : α),
  limsup (fun (i : ι) ↦ u i a) cofinite < h.some (s := Set.Ioo c b) →
    limsup (fun (x : ι) ↦ u x a) cofinite ≤ h.some (s := Set.Ioo c b)
Tactic: filter_upwards [(tendsto_order.1 h_limsup).2 _ h.some_mem.1] with r hr using hr.le
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : ¬(Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ c
have h₁ : ∀ (r : α) (hr : limsup (fun (i : ι) ↦ u i r) cofinite < b), limsup (fun (x : ι) ↦ u x r) cofinite ≤ c
Tactic: filter_upwards [(tendsto_order.1 h_limsup).2 b hb] with r hr
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : ¬(Set.Ioo c b).Nonempty
r : α
hr : limsup (fun (i : ι) ↦ u i r) cofinite < b
⊢ limsup (fun (x : ι) ↦ u x r) cofinite ≤ c
have h₁ : ∀ (h : c < limsup (fun (x : ι) ↦ u x r) cofinite), (Set.Ioo c b).Nonempty
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
have this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
Tactic: have : ∀ᶠ r in atTop, limsup (u · r) cofinite ≤ b' := by
    simp only [b']
    split_ifs with h
    · filter_upwards [(tendsto_order.1 h_limsup).2 _ h.some_mem.1] with r hr using hr.le
    · filter_upwards [(tendsto_order.1 h_limsup).2 b hb] with r hr
      contrapose! h
      exact ⟨limsup (u · r) cofinite, h, hr⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
have inr : ∀ (r : α) (hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
Tactic: obtain ⟨r, hr⟩ : ∃ r, ∀ s ≥ r, limsup (u · s) cofinite ≤ b' := by simpa using this
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
have inl : ∀ (h : Set.Ioo b' b = ∅), ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
Tactic: rcases Set.eq_empty_or_nonempty (Set.Ioo b' b) with h | ⟨b'', hb'b'', hb''b⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
inl : ∀ (h : Set.Ioo b' b = ∅), ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
have inr : ∀ (b'' : β) (hb'b'' : b' < b'') (hb''b : b'' < b), ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
Tactic: rcases Set.eq_empty_or_nonempty (Set.Ioo b' b) with h | ⟨b'', hb'b'', hb''b⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
have inl : ∀ᶠ (n : ι) in cofinite, u n r ≤ b'
Tactic: refine ⟨b', ⟨le_rfl, hb'b⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b'
have h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
Tactic: have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b'
have h₁ : ∀ (n : ι) (hn : u n r < b), u n r ≤ b'
Tactic: filter_upwards [h_lt] with n hn
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
n : ι
hn : u n r < b
⊢ u n r ≤ b'
have h₁ : ∀ (h : b' < u n r), (Set.Ioo b' b).Nonempty
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
have inr : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
Tactic: refine ⟨b'', ⟨hb'b''.le, hb''b⟩ , ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
have h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b''
Tactic: have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b'')
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b''
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ u a r < b'') x} x →
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ u n r ≤ b'') x} x}
    a
Tactic: filter_upwards [h_lt] with n hn using hn.le
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b''
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ u a r < b'') x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ u n r ≤ b'') x} x}
      a
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
have h₁ : ∀ (a : ι), u a r < b'' → u a r ≤ b''
Tactic: filter_upwards [h_lt] with n hn using hn.le
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
have inr : ∀ (b'' : β) (hb''b : b'' ∈ Set.Ico b' b) (hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''),
  ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
Tactic: obtain ⟨b'', hb''b, hb''⟩ : ∃ b'' ∈ Set.Ico b' b, ∀ᶠ n in cofinite, u n r ≤ b'' := by
    rcases Set.eq_empty_or_nonempty (Set.Ioo b' b) with h | ⟨b'', hb'b'', hb''b⟩
    · refine ⟨b', ⟨le_rfl, hb'b⟩, ?_⟩
      have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b)
      filter_upwards [h_lt] with n hn
      contrapose! h
      exact ⟨u n r, h, hn⟩
    · refine ⟨b'', ⟨hb'b''.le, hb''b⟩ , ?_⟩
      have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b'')
      filter_upwards [h_lt] with n hn using hn.le
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this_1 : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
this : ∀ᶠ (r : α) in atTop, u n r ≤ b'
⊢ ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
have this₁ : ∃ (a : α), ∀ (b : α), a ≤ b → u n b ≤ b'
Tactic: simp only [eventually_atTop, ge_iff_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this_1 : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
this : ∃ (a : α), ∀ (b : α), a ≤ b → u n b ≤ b'
⊢ ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
have rcases : ∀ (r : α) (hr : ∀ (b : α), r ≤ b → u n b ≤ b'), ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
Tactic: rcases this with ⟨r, hr⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
⊢ ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
have suffices : ∀ᶠ (r : α) in atTop, u n r ≤ b'
Tactic: suffices ∀ᶠ r in atTop, u n r ≤ b' by
      simp only [eventually_atTop, ge_iff_le] at this
      rcases this with ⟨r, hr⟩
      exact ⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
have pos : ∀ (h : (Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, u n r ≤ h.some (s := Set.Ioo c b)
Tactic: split_ifs with h