α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => balanceL (insert' x l) y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => balanceR l y (insert' x r)) =
    match cmpLE x y with
    | Ordering.lt => balanceL (insertWith id x l) y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => balanceR l y (insertWith id x r)
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ insert' x (node size✝ l y r) = insertWith id x (node size✝ l y r)
unfold insert' insertWith
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => balanceL (insert' x l) y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => balanceR l y (insert' x r)) =
    match cmpLE x y with
    | Ordering.lt => balanceL (insertWith id x l) y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => balanceR l y (insertWith id x r)
cases cmpLE x y <;> simp [insert'_eq_insertWith]