∀ (β : Type u_3) (γ : Type u_4) [inst : ConditionallyCompleteLinearOrderedField β]
  [inst_1 : ConditionallyCompleteLinearOrderedField γ],
  ⇑(LinearOrderedField.inducedOrderRingIso β γ) = LinearOrderedField.inducedMap β γ