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
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 : ι
pos : ∀ (h : (Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, u n r ≤ h.some (s := Set.Ioo c b)
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ 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, u n r ≤ 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
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 : ι
h : (Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ h.some (s := Set.Ioo c b)
have h₁ : ∀ (r : α) (hr : u n r < h.some (s := Set.Ioo c b)), u n r ≤ h.some (s := Set.Ioo c b)
Tactic: filter_upwards [(tendsto_order.1 (h_all n)).2 _ h.some_mem.1] 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
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 : ι
h : ¬(Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ c
have h₁ : ∀ (r : α) (hr : u n r < b), u n r ≤ c
Tactic: filter_upwards [(tendsto_order.1 (h_all n)).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
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
h : ¬(Set.Ioo c b).Nonempty
r : α
hr : u n r < b
⊢ u n r ≤ c
have h₁ : ∀ (h : c < u n r), (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
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''
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
have A : ∀ (n : ι), ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
Tactic: have A (n) : ∃ r, ∀ s ≥ r, u n s ≤ b'' := by
    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⟩
    simp only [b']
    split_ifs with h
    · filter_upwards [(tendsto_order.1 (h_all n)).2 _ h.some_mem.1] with r hr
      exact hr.le
    · filter_upwards [(tendsto_order.1 (h_all n)).2 b hb] with r hr
      contrapose! h
      exact ⟨u n r, 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'
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''
A : ∀ (n : ι), ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
have inr : ∀ (rs : (n : ι) → α) (hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
Tactic: choose rs hrs using A
Cleared hypotheses: A
-- 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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
have inr : ∃ (a : α), ∀ (b_1 : α), a ≤ b_1 → ⨆ (i : ι), u i b_1 < b
Tactic: simp only [eventually_atTop, ge_iff_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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
⊢ ∃ (a : α), ∀ (b_1 : α), a ≤ b_1 → ⨆ (i : ι), u i b_1 < b
have inr : ∀ (v : α) (hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v), ⨆ (i : ι), u i v < b
Tactic: refine ⟨r ⊔ ⨆ n : {n | b'' < u n r}, rs n, fun v hv ↦ ?_⟩
-- 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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
⊢ ⨆ (i : ι), u i v < b
have apply : ∀ (n : ι), u n v ≤ b''
Tactic: apply lt_of_le_of_lt (iSup_le fun n ↦ ?_) hb''b.2
-- 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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
⊢ u n v ≤ b''
have pos : ∀ (hn : b'' < u n r), u n v ≤ b''
Tactic: by_cases hn : b'' < u n r
-- 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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
pos : ∀ (hn : b'' < u n r), u n v ≤ b''
⊢ u n v ≤ b''
have neg : ∀ (hn : ¬b'' < u n r), u n v ≤ b''
Tactic: by_cases hn : b'' < u n r
-- 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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
hn : b'' < u n r
⊢ u n v ≤ b''
have pos : v ≥ rs n
Tactic: refine hrs n v ?_
-- 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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
hn : b'' < u n r
⊢ rs (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {n : ι | b'' < u n r} x) n hn) : ι) ≤
    ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι)
have refine : BddAbove.{u_7} (α := α) (Set.range fun (x : (↑{n : ι | b'' < u n r} : Type u_1)) ↦ rs (↑x : ι))
Tactic: refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})
-- 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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
hn : b'' < u n r
⊢ BddAbove.{u_7} (α := α) (Set.range fun (x : (↑{n : ι | b'' < u n r} : Type u_1)) ↦ rs (↑x : ι))
have this₁ : Finite.{u_1 + 1} (↑{n : ι | b'' < u n r} : Type u_1)
Tactic: have : Finite {n | b'' < u n r} := by simpa using 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
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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
hn : b'' < u n r
⊢ v ≥ rs n
have calc : rs (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {n : ι | b'' < u n r} x) n hn) : ι) ≤
  ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι)
Tactic: calc rs n
    _ = rs (⟨n, by simp [hn]⟩ : {n | b'' < u n r}) := rfl
    _ ≤ ⨆ n : {n | b'' < u n r}, rs n := by
      refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})
      have : Finite {n | b'' < u n r} := by simpa using hb''
      exact Finite.bddAbove_range _
    _ ≤ r ⊔ ⨆ n : {n | b'' < u n r}, rs n := le_sup_right
    _ ≤ v := hv
-- 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''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
hn : ¬b'' < u n r
⊢ u n v ≤ b''
have neg : r ≤ v
Tactic: refine (h_anti n ?_).trans (not_lt.mp hn)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ℕ → α → β
c : β
h_all : ∀ (n : ℕ), Tendsto (u n) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (n : ℕ) ↦ u n r) atTop) atTop (𝓝 c)
h_anti : ∀ (n : ℕ), Antitone (u n)
⊢ Tendsto (fun (r : α) ↦ ⨆ (n : ℕ), u n r) atTop (𝓝 c)
have h_limsup₁ : Tendsto (fun (r : α) ↦ limsup (fun (n : ℕ) ↦ u n r) cofinite) atTop (𝓝 c)
Tactic: rw [← cofinite_eq_atTop] at h_limsup
Cleared hypotheses: h_limsup, h_anti
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
⊢ f F.limsSup = liminf f F
have a : f F.limsSup ≤ liminf f F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
a : f F.limsSup ≤ liminf f F
⊢ f F.limsSup = liminf f F
have a₁ : liminf f F ≤ f F.limsSup
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
⊢ f F.limsSup ≤ liminf f F
have a : sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F
Tactic: rw [limsSup, f_decr.map_csInf_of_continuousAt f_cont bdd_above cobdd]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
⊢ sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F
have a : ∀ c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}), c < liminf f F
Tactic: apply le_of_forall_lt
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < liminf f F
have a : c < sSup {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
Tactic: simp only [liminf, limsInf, eventually_map] at hc ⊢
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < sSup {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
have a : ∀ (d : S) (hd : d ∈ f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}) (h'd : c < d),
  c < sSup {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
Tactic: obtain ⟨d, hd, h'd⟩ :=
      exists_lt_of_lt_csSup (bdd_above.recOn fun x hx ↦ ⟨f x, Set.mem_image_of_mem f hx⟩) hc
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ c < sSup {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
have apply : BddAbove.{u_5} (α := S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
Tactic: apply lt_csSup_of_lt ?_ ?_ h'd
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
apply : BddAbove.{u_5} (α := S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
⊢ c < sSup {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
have apply₁ : Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d
Tactic: apply lt_csSup_of_lt ?_ ?_ h'd
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d
have rcases : ∀ (e : R) (he : Membership.mem (γ := Set R) {a : R | ∀ᶠ (n : R) in F, n ≤ a} e) (fe_eq_d : f e = d),
  Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d
Tactic: rcases hd with ⟨e, ⟨he, fe_eq_d⟩⟩
Cleared hypotheses: hd