-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem All.balLeft
    (hl : l.All p) (hv : p v) (hr : r.All p) : (balLeft l v r).All p

Proof state:
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
⊢ All p (l.balLeft v r)

Tactic:
unfold balLeft

Result:
α✝ : 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 => 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)

Proof state:
α✝ : 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 => 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)

Tactic:
split <;> (try simp_all)

Result:
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), ¬l = node red a x b
⊢ All p
    (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)

Proof state:
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), ¬l = node red a x b
⊢ All p
    (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)

Tactic:
split <;> simp_all [All.setRed]

Result:
no goals

Proof state:
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), l = node red a x b → False
⊢ All p
    (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)

Tactic:
simp_all

Result:
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), ¬l = node red a x b
⊢ All p
    (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)

Proof state:
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), l = node red a x b → False
⊢ All p
    (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)

Tactic:
try simp_all

Result:
case h_2
α✝ : Type u_1
p : α✝ → Prop
l : RBNode α✝
v : α✝
r : RBNode α✝
hl : All p l
hv : p v
hr : All p r
l✝ : RBNode α✝
x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), ¬l = node red a x b
⊢ All p
    (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)