Rat.floor_cast

theorem Rat.floor_cast : ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌊↑x⌋ = ⌊x⌋ := by sorry

This theorem states that for any rational number `x` and for any type `α` that is a linear ordered field and has a floor function, the floor of the real number equivalent of `x` (denoted `↑x`) is equal to the floor of `x` itself. In other words, casting a rational number to a real number does not change the result of taking the floor of that number.

More concisely: For any rational number `x` and linear ordered field `α` with a floor function, `⌊x⌋ = ⌊Reál x⌋`, where `x` is the rational number, `Reál x` is the real number equivalent of `x`, `⌊x⌋` is the floor of `x`, and `⌊Reál x⌋` is the floor of the real number `Reál x`.