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