awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LiminfLimsup
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''

Tactic:
hrs n v ?_
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
pos : v ≥ rs n
⊢ u n v ≤ b''

Tactic:
refine hrs n v ?_
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ Membership.mem (γ := Set ι) {n : ι | b'' < u n r} n

Tactic:
simp [hn]
-- Module: Mathlib.Topology.Order.LiminfLimsup
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 n = rs (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {n : ι | b'' < u n r} x) n hn) : ι)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
refine : BddAbove.{u_7} (α := α) (Set.range fun (x : (↑{n : ι | b'' < u n r} : Type u_1)) ↦ rs (↑x : ι))
⊢ 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:
refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})

Premises used: Subtype.mk, le_ciSup
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ Finite.{u_1 + 1} (↑{n : ι | b'' < u n r} : Type u_1)

Tactic:
simpa using hb''
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ Finite.{u_1 + 1} (↑{n : ι | b'' < u n r} : Type u_1)

Tactic:
have : Finite {n | b'' < u n r} := by simpa using hb''
-- Module: Mathlib.Topology.Order.LiminfLimsup
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''
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
this : Finite.{u_1 + 1} (↑{n : ι | b'' < u n r} : Type u_1)
⊢ BddAbove.{u_7} (α := α) (Set.range fun (x : (↑{n : ι | b'' < u n r} : Type u_1)) ↦ rs (↑x : ι))

Tactic:
Finite.bddAbove_range _

Premises used: Finite.bddAbove_range
-- Module: Mathlib.Topology.Order.LiminfLimsup
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''
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
this : Finite.{u_1 + 1} (↑{n : ι | b'' < u n r} : Type u_1)
⊢ BddAbove.{u_7} (α := α) (Set.range fun (x : (↑{n : ι | b'' < u n r} : Type u_1)) ↦ rs (↑x : ι))

Tactic:
exact Finite.bddAbove_range _

Premises used: Finite.bddAbove_range
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤
    r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι)

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v

Tactic:
hv
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
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 : ι)
⊢ v ≥ 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

Premises used: le_sup_right, Subtype.mk, Subtype.val, rfl
-- Module: Mathlib.Topology.Order.LiminfLimsup
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''

Tactic:
(h_anti n ?_).trans (not_lt.mp hn)

Premises used: not_lt, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
neg : r ≤ v
⊢ u n v ≤ b''

Tactic:
refine (h_anti n ?_).trans (not_lt.mp hn)

Premises used: not_lt, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ r ≤ r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι)

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v

Tactic:
hv
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
⊢ r ≤ v

Tactic:
calc r
    _ ≤ r ⊔ ⨆ n : {n | b'' < u n r}, rs n := le_sup_left
    _ ≤ v := hv

Premises used: le_sup_left
-- Module: Mathlib.Topology.Order.LiminfLimsup
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 : α) ↦ limsup (fun (n : ℕ) ↦ u n r) cofinite) atTop (𝓝 c)

Tactic:
rw [← cofinite_eq_atTop] at h_limsup

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Topology.Order.LiminfLimsup
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)
h_limsup₁ : Tendsto (fun (r : α) ↦ limsup (fun (n : ℕ) ↦ u n r) cofinite) atTop (𝓝 c)
⊢ ∀ (n : ℕ), Antitone (u n)

Tactic:
rw [← cofinite_eq_atTop] at h_limsup

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Topology.Order.LiminfLimsup
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) cofinite) atTop (𝓝 c)
h_anti : ∀ (n : ℕ), Antitone (u n)
⊢ Tendsto (fun (r : α) ↦ ⨆ (n : ℕ), u n r) atTop (𝓝 c)

Tactic:
_root_.tendsto_iSup_of_tendsto_limsup h_all h_limsup h_anti

Premises used: tendsto_iSup_of_tendsto_limsup
-- Module: Mathlib.Topology.Order.LiminfLimsup
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) cofinite) atTop (𝓝 c)
h_anti : ∀ (n : ℕ), Antitone (u n)
⊢ Tendsto (fun (r : α) ↦ ⨆ (n : ℕ), u n r) atTop (𝓝 c)

Tactic:
exact _root_.tendsto_iSup_of_tendsto_limsup h_all h_limsup h_anti

Premises used: tendsto_iSup_of_tendsto_limsup
-- Module: Mathlib.Topology.Order.LiminfLimsup
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
a₁ : liminf f F ≤ f F.limsSup
⊢ f F.limsSup = liminf f F

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Order.LiminfLimsup
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 : sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F
⊢ f F.limsSup ≤ liminf f F

Tactic:
rw [limsSup, f_decr.map_csInf_of_continuousAt f_cont bdd_above cobdd]

Premises used: Filter.limsSup, Antitone.map_csInf_of_continuousAt
-- Module: Mathlib.Topology.Order.LiminfLimsup
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 : ∀ c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}), c < liminf f F
⊢ sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F

Tactic:
apply le_of_forall_lt

Premises used: le_of_forall_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
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})
a : c < sSup {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
⊢ c < liminf f F

Tactic:
simp only [liminf, limsInf, eventually_map] at hc ⊢

Premises used: Filter.limsInf, Filter.liminf, Filter.eventually_map
-- Module: Mathlib.Topology.Order.LiminfLimsup
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})
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}
⊢ 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

Premises used: exists_lt_of_lt_csSup, Exists.recOn