no goals
F : Type ?u.23977
α : Type ?u.23980
β : Type u_1
γ : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
b : β
⊢ inducedMap γ β (inducedMap β γ b) = b
rw [inducedMap_inducedMap, inducedMap_self]