α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
⊢ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop} =
    {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
⊢ limsup s atTop = {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
rw [limsup_eq_tendsto_sum_indicator_nat_atTop s]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop} ↔
    ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
⊢ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop} =
    {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
ext ω
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
    Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop} ↔
    ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
simp only [Set.mem_setOf_eq]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
    Tendsto (fun n => ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)) atTop atTop

α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) = fun n =>
    ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
    Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop
rw [(_ : (fun n ↦ ∑ k in Finset.range n, (s (k + 1)).indicator (1 : α → R) ω) = fun n ↦
  ↑(∑ k in Finset.range n, (s (k + 1)).indicator (1 : α → ℕ) ω))]
no goals
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
    Tendsto (fun n => ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)) atTop atTop
exact tendsto_nat_cast_atTop_iff.symm
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
n : ℕ
⊢ ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω = ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) = fun n =>
    ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
ext n
no goals
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
n : ℕ
⊢ ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω = ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
simp only [Set.indicator, Pi.one_apply, Finset.sum_boole, Nat.cast_id]