no goals
α : Type u_1
β : Type u_2
cmpα : α → α → Ordering
cmpβ : β → β → Ordering
f : α → β
inst✝ : IsMonotone cmpα cmpβ f
c✝ : RBColor
a : RBNode α
x : α
b : RBNode α
ax : All (fun x_1 => cmpLT cmpα x_1 x) a
xb : All (fun x_1 => cmpLT cmpα x x_1) b
ha : Ordered cmpα a
hb : Ordered cmpα b
⊢ Ordered cmpβ (map f (node c✝ a x b))
refine ⟨ax.map ?_, xb.map ?_, ha.map f, hb.map f⟩ <;> exact IsMonotone.lt_mono