-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Balanced.balLeft (hl : l.RedRed True n) (hr : r.Balanced cr (n + 1)) :
    (balLeft l v r).RedRed (cr = red) (n + 1)

Proof state:
α✝ : Type u_1
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hr : r.Balanced 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)

Tactic:
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)

Result:
no goals

Proof state:
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : r.Balanced cr (n + 1)
⊢ RedRed (cr = red) (l.balLeft v r) (n + 1)

Tactic:
unfold balLeft

Result:
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : r.Balanced 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 => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r)
    (n + 1)

Proof state:
case h_1
α✝ : Type u_1
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hr : r.Balanced 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)

Tactic:
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)

Result:
no goals

Proof state:
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : r.Balanced 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 => l.balance2 v (node red a y b)
    | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
    | r => node red l v r)
    (n + 1)

Tactic:
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

Result:
no goals

Proof state:
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : r.Balanced 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 => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r)
    (n + 1)

Tactic:
split

Result:
case h_1
α✝ : Type u_1
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hr : r.Balanced 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 : r.Balanced 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 => l.balance2 v (node red a y b)
    | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
    | r => node red l v r)
    (n + 1)

Proof state:
case h_2
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cr : RBColor
n : Nat
hl : RedRed True l n
hr : r.Balanced 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 => l.balance2 v (node red a y b)
    | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
    | r => node red l v r)
    (n + 1)

Tactic:
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

Result:
no goals