Int.cast in equations

Stream: new members

[Junjie Bai]

How can I prove that :

example (u : ℤ) : ⌈u⌉ = ⌊u⌋ + 1 ↔ (⌈u⌉ : ℚ)= (⌊u⌋ : ℚ) + 1 := by sorry

[Riccardo Brasca]

You can use exact_mod_cast, it should be immediate.

[Riccardo Brasca]

Even

example (u : ℤ) : ⌈u⌉ = ⌊u⌋ + 1 ↔ (⌈u⌉ : ℚ)= (⌊u⌋ : ℚ) + 1 := by simp

might work

[Junjie Bai]

That totally solve my problem, thank you very much!!