α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
⊢ All p
    (match r with
    | node red b y c => node red l v (node black b y c)
    | r =>
      match l with
      | node black a x b => balance1 (node red a x b) v r
      | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
      | l => 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 (balRight l v r)
unfold balRight
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 α✝), r = node red a x b → False
⊢ All p
    (match l with
    | node black a x b => balance1 (node red a x b) v r
    | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
    | l => 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 r with
    | node red b y c => node red l v (node black b y c)
    | r =>
      match l with
      | node black a x b => balance1 (node red a x b) v r
      | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
      | l => 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 α✝), r = node red a x b → False
⊢ All p
    (match l with
    | node black a x b => balance1 (node red a x b) v r
    | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
    | l => node red l v r)
split <;> simp_all [All.setRed]