Problem by rounding

Stream: lean4

[Leni Greco]

hello!
I have problems working with ↑q . What do I have to change, so that I don't get errors?

import LeanCourse.Common
import LeanCourse.MIL.C03_Logic.solutions.Solutions_S06_Sequences_and_Convergence
set_option linter.unusedVariables false
open Nat Real Function Set


lemma : SequentialLimit (fun n ↦ 1 / (n+1)) 0 := by
   intros a b
   have ha: a>0 := by assumption
   use (⌈1/a⌉₊ : ℕ)
   simp
   intro q w
   have h1: |(↑q + 1)⁻¹|=(↑q + 1)⁻¹:= by exact sorry
   sorry

[Eric Wieser]

Unfortunately this isn't a #mwe because it uses LeanCourse, which most of us don't have because we're not on your course!

[Damiano Testa]

Taking into account what Eric said, you could see if using a type ascription similar to the one you used in the use line and removing the ↑ helps... : smile