Stating 'limsup X_n / a_n = 1 a.s.' in Lean without boundedness side goals: use EReal

For almost-sure limsup theorems such as the law of the iterated logarithm, state limsup (fun n ↦ ((X n ω / a n : ℝ) : EReal)) atTop = 1. In EReal the IsBounded/IsCobounded arguments are discharged by isBoundedDefault. Upper bound: rw [← EReal.coe_one], then ge_of_tendsto' (EReal.tendsto_coe.2 h) along 1 + 1/(k+1) -> 1, then limsup_le_of_le (by isBoundedDefault). Lower bound: le_of_tendsto' along 1 - 1/(k+2) with le_limsup_of_frequently_le _ (by isBoundedDefault). Push each pointwise bound through EReal.coe_le_coe_iff.2 ((div_le_iff₀ hpos).2 h), where hpos says a n > 0 eventually. Get all k at once with ae_all_iff. To read it back, frequently_lt_of_lt_limsup (by isBoundedDefault) turns limsup = 1 into 'frequently > 1/2', and EReal.limsup_neg gives the liminf of -X. Note the direction: ge_of_tendsto' proves limsup ≤ 1 and le_of_tendsto' proves 1 ≤ limsup. I had them swapped.