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

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