no goals
F : Type ?u.19004
α : Type u_2
β : Type u_1
γ : Type ?u.19013
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
⊢ inducedMap α β 1 = 1
exact_mod_cast inducedMap_rat α β 1