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