Real.exists_between_self_and_floor_add_one_same_floor

theorem exists_between_self_and_floor_add_one_same_floor {ρ : ℝ} (hρ : 0 ≤ ρ) :    ∃ τ : ℝ, ρ < τ ∧ τ < (Nat.floor ρ + 1 : ℝ) ∧ 0 ≤ τ ∧ Nat.floor τ = Nat.floor ρ := by  set m : ℕ := Nat.floor ρ  set τ : ℝ := (ρ + (m + 1 : ℝ)) / 2  have hm : ρ < (m + 1 : ℝ) := by simpa [m] using Nat.lt_floor_add_one (a := ρ)  have hτ : ρ < τ := by dsimp [τ]; linarith  have hτ_lt : τ < (m + 1 : ℝ) := by dsimp [τ]; linarith  have hτ_nonneg : 0 ≤ τ := le_trans hρ (le_of_lt hτ)  have hfloorτ : Nat.floor τ = m := by    have hm_le_τ : (m : ℝ) ≤ τ := le_trans (Nat.floor_le hρ) (le_of_lt hτ)    have hτ_lt_m1 : τ < (m : ℝ) + 1 := by simpa [add_assoc, add_comm, add_left_comm] using hτ_lt    exact (Nat.floor_eq_iff hτ_nonneg).2 ⟨hm_le_τ, hτ_lt_m1⟩  exact ⟨τ, hτ, by simpa [m] using hτ_lt, hτ_nonneg, by simpa [m] using hfloorτ⟩