no goals
F : Type ?u.9759
α : Type u_2
β : Type u_1
γ : Type ?u.9768
inst✝¹ : LinearOrderedField α
inst✝ : LinearOrderedField β
a a₁ a₂ : α
b : β
q✝ q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}
simp_rw [cutMap, Rat.cast_lt]