α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
⊢ All p
    (match l with
    | node red a x b => node red (node black a x b) v r
    | l =>
      match r with
      | node black a y b => balance2 l v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (balance2 b z (setRed c))
      | r => node red l v r)
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
⊢ All p (balLeft l v r)
unfold balLeft
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r l✝ : RBNode α✝
hl : All p l
hv : p v
hr : All p r
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), l = node red a x b → False
⊢ All p
    (match r with
    | node black a y b => balance2 l v (node red a y b)
    | node red (node black a y b) z c => node red (node black l v a) y (balance2 b z (setRed c))
    | r => node red l v r)
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
⊢ All p
    (match l with
    | node red a x b => node red (node black a x b) v r
    | l =>
      match r with
      | node black a y b => balance2 l v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (balance2 b z (setRed c))
      | r => node red l v r)
split <;> simp_all
no goals
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r l✝ : RBNode α✝
hl : All p l
hv : p v
hr : All p r
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), l = node red a x b → False
⊢ All p
    (match r with
    | node black a y b => balance2 l v (node red a y b)
    | node red (node black a y b) z c => node red (node black l v a) y (balance2 b z (setRed c))
    | r => node red l v r)
split <;> simp_all [All.setRed]