α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hr : Balanced r c n
⊢ (match l, v, r with
    | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d)
    | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
    | a, x, b => node black a x b) =
    node black l v r
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hr : Balanced r c n
⊢ balance2 l v r = node black l v r
unfold balance2
no goals
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hr : Balanced r c n
⊢ (match l, v, r with
    | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d)
    | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
    | a, x, b => node black a x b) =
    node black l v r
split <;> first | rfl | match hr with.
no goals
case h_3
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hr : Balanced r c n
x✝⁴ : RBNode α
x✝³ : α
x✝² : RBNode α
x✝¹ : ∀ (b : RBNode α) (y : α) (c : RBNode α) (z : α) (d : RBNode α), r = node red (node red b y c) z d → False
x✝ : ∀ (b : RBNode α) (y : α) (c : RBNode α) (z : α) (d : RBNode α), r = node red b y (node red c z d) → False
⊢ node black l v r = node black l v r
rfl
no goals
case h_2
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
x✝³ : RBNode α
x✝² : α
x✝¹ b✝ : RBNode α
y✝ : α
c✝ : RBNode α
z✝ : α
d✝ : RBNode α
x✝ : ∀ (b : RBNode α) (y : α) (c : RBNode α), b✝ = node red b y c → False
hr : Balanced (node red b✝ y✝ (node red c✝ z✝ d✝)) c n
⊢ node red (node black l v b✝) y✝ (node black c✝ z✝ d✝) = node black l v (node red b✝ y✝ (node red c✝ z✝ d✝))
match hr with.