∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (iso : α ≃ β)
  (h : ∀ {a b : α}, iso a ≤ iso b ↔ a ≤ b),
  OrderIso.withBotCongr { toEquiv := iso, map_rel_iff' := h } =
    { toFun := WithBot.map ⇑{ toEquiv := iso, map_rel_iff' := h },
      invFun := { toEquiv := iso, map_rel_iff' := ⋯ }.withBotCongr.invFun, left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }