-- 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)
inl : ∀ (hι : IsEmpty ι), Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
inr inr₁ : ∀ (n0 : ι), Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
inr₂ : ∀ (n0 : ι) (b : β) (hb : b < c), ∀ᶠ (b_1 : α) in atTop, b < ⨆ (i : ι), u i b_1
inr₃ inr₄ : ∀ (n0 : ι) (b : β) (hb : b > c), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
inr₅ : ∀ (n0 : ι) (b : β) (hb : b > c), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
inr₆ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
inr₇ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
inr₈ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
inr₉ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
inr₁₀ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
inr₁₁ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
inr₁₂ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
inr₁₃ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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
rcases :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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''
pos :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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''
neg neg₁ :
  ∀ (n0 : ι) (b : β) (hb : b > c),
    let 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''
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)

Tactic:
classical
  rcases isEmpty_or_nonempty ι with hι | ⟨⟨n0⟩⟩
  · simpa using h_limsup
  refine tendsto_order.mpr ⟨fun b hb ↦ ?_, fun b hb ↦ ?_⟩
  · filter_upwards with r
    have : c ≤ u n0 r := (h_anti n0).le_of_tendsto (h_all n0) r
    exact hb.trans_le (this.trans (le_iSup_iff.mpr fun b a ↦ a n0))
  -- `⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ i, u i b_1 < b` for `b > c`
  let b' := if h : (Set.Ioo c b).Nonempty then h.some else c
  have hb'b : b' < b := by
    simp only [b']
    split_ifs with h
    exacts [h.some_mem.2, hb]
  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⟩
  obtain ⟨r, hr⟩ : ∃ r, ∀ s ≥ r, limsup (u · s) cofinite ≤ b' := by simpa using this
  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
  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⟩
  choose rs hrs using A
  simp only [eventually_atTop, ge_iff_le]
  refine ⟨r ⊔ ⨆ n : {n | b'' < u n r}, rs n, fun v hv ↦ ?_⟩
  -- `⊢ ⨆ i, u i v < b`
  apply lt_of_le_of_lt (iSup_le fun n ↦ ?_) hb''b.2
  -- `⊢ u n v ≤ b''` for `v` such that `r ⊔ (⨆ n, rs n) ≤ v`
  by_cases hn : b'' < u n r
  · refine hrs n v ?_
    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
  · refine (h_anti n ?_).trans (not_lt.mp hn)
    calc r
    _ ≤ r ⊔ ⨆ n : {n | b'' < u n r}, rs n := le_sup_left
    _ ≤ v := hv

Premises used: Iff.mpr, le_sup_left, ge_iff_le, tendsto_order, isEmpty_or_nonempty, le_sup_right, And.intro, Filter.cofinite, Filter.eventually_atTop, rfl