no goals
F : Type u_3
ι : Type ?u.80063
α : Type u_1
β : Type u_2
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ ↑f ↑q = ↑q
rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]