α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : Balanced r cr (n + 1)
⊢ RedRed (cr = red)
    (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)
    (n + 1)
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : Balanced r cr (n + 1)
⊢ RedRed (cr = red) (balLeft l v r) (n + 1)
unfold balLeft
case h_1
α✝ : Type u_1
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hr : Balanced r cr (n + 1)
l✝ a✝ : RBNode α✝
x✝ : α✝
b✝ : RBNode α✝
hl : RedRed True (node red a✝ x✝ b✝) n
⊢ RedRed (cr = red) (node red (node black a✝ x✝ b✝) v r) (n + 1)

case h_2
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : Balanced r cr (n + 1)
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), l = node red a x b → False
⊢ RedRed (cr = red)
    (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)
    (n + 1)
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : Balanced r cr (n + 1)
⊢ RedRed (cr = red)
    (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)
    (n + 1)
split
no goals
case h_1
α✝ : Type u_1
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hr : Balanced r cr (n + 1)
l✝ a✝ : RBNode α✝
x✝ : α✝
b✝ : RBNode α✝
hl : RedRed True (node red a✝ x✝ b✝) n
⊢ RedRed (cr = red) (node red (node black a✝ x✝ b✝) v r) (n + 1)
next a x b => exact
let ⟨ca, cb, ha, hb⟩ := hl.of_red
match cr with
| red => .redred rfl (.black ha hb) hr
| black => .balanced (.red (.black ha hb) hr)
no goals
α✝ : Type u_1
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hr : Balanced r cr (n + 1)
l✝ a : RBNode α✝
x : α✝
b : RBNode α✝
hl : RedRed True (node red a x b) n
⊢ RedRed (cr = red) (node red (node black a x b) v r) (n + 1)
exact
let ⟨ca, cb, ha, hb⟩ := hl.of_red
match cr with
| red => .redred rfl (.black ha hb) hr
| black => .balanced (.red (.black ha hb) hr)
no goals
case h_2
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : Balanced r cr (n + 1)
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), l = node red a x b → False
⊢ RedRed (cr = red)
    (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)
    (n + 1)
next H => exact match hl with
| .redred .. => nomatch H _ _ _ rfl
| .balanced hl => match hr with
  | .black ha hb =>
    let ⟨c, h⟩ := RedRed.balance2 hl (.redred trivial ha hb); .balanced h
  | .red (.black ha hb) (.black hc hd) =>
    let ⟨c, h⟩ := RedRed.balance2 hb (.redred trivial hc hd); .redred rfl (.black hl ha) h
no goals
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : Balanced r cr (n + 1)
l✝ : RBNode α✝
H : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), l = node red a x b → False
⊢ RedRed (cr = red)
    (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)
    (n + 1)
exact match hl with
| .redred .. => nomatch H _ _ _ rfl
| .balanced hl => match hr with
| .black ha hb =>
let ⟨c, h⟩ := RedRed.balance2 hl (.redred trivial ha hb); .balanced h
| .red (.black ha hb) (.black hc hd) =>
let ⟨c, h⟩ := RedRed.balance2 hb (.redred trivial hc hd); .redred rfl (.black hl ha) h