RS_prime.leftLim_theta_succ

lemma leftLim_theta_succ (k : ℕ) : Function.leftLim θ (k + 1) = θ k := by  rw [leftLim_eq_of_tendsto (y := θ ↑k)]  · rw [nhdsWithin_restrict (t := Set.Ioo ↑k ↑(k + 2))]    · rw [Set.Iio_inter_Ioo]      apply tendsto_nhdsWithin_congr (f := fun _ => θ ↑k)      · intro y hy        have floor_k_eq: ⌊(k : ℝ)⌋₊ = ⌊(y: ℝ)⌋₊ := by          rw [eq_comm, Nat.floor_eq_iff]          · simp            grind          · simp at hy            linarith        rw [Chebyshev.theta_eq_theta_coe_floor]        rw [Chebyshev.theta_eq_theta_coe_floor (x := y)]        congr      · simp    · simp    · exact isOpen_Ioo