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

Proof state:
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (b✝.append c✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

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

Result:
no goals

Proof state:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Tactic:
have ⟨hy, hc, hd⟩ := hr

Result:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Proof state:
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Tactic:
have := hb.append hc

Result:
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (b✝.append c✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Proof state:
α✝ : Type u_1
l r : RBNode α✝
p : α✝ → Prop
hl : All p l
hr : All p r
⊢ All p
    (match l, r with
    | nil, x => x
    | x, nil => x
    | node red a x b, node red c y d =>
      match b.append c with
      | node red b' z c' => node red (node red a x b') z (node red c' y d)
      | bc => node red a x (node red bc y d)
    | node black a x b, node black c y d =>
      match b.append c with
      | node red b' z c' => node red (node black a x b') z (node black c' y d)
      | bc => a.balLeft x (node black bc y d)
    | a@h:(node black l v r), node red b x c => node red (a.append b) x c
    | node red a x b, c@h:(node black l v r) => node red a x (b.append c))

Tactic:
split <;> try simp [*]

Result:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

case h_5
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ l✝ : RBNode α✝
v✝ : α✝
r✝ b✝ : RBNode α✝
x✝ : α✝
c✝ : RBNode α✝
hl : All p (node black l✝ v✝ r✝)
hr : All p (node red b✝ x✝ c✝)
⊢ p x✝ ∧ All p ((node black l✝ v✝ r✝).append b✝) ∧ All p c✝

case h_6
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node black l✝ v✝ r✝)
⊢ p x✝ ∧ All p a✝ ∧ All p (b✝.append (node black l✝ v✝ r✝))

Proof state:
case h_6
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node black l✝ v✝ r✝)
⊢ All p (node red a✝ x✝ (b✝.append (node black l✝ v✝ r✝)))

Tactic:
simp [*]

Result:
case h_6
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node black l✝ v✝ r✝)
⊢ p x✝ ∧ All p a✝ ∧ All p (b✝.append (node black l✝ v✝ r✝))

Proof state:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (b✝.append c✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case h_6
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node black l✝ v✝ r✝)
⊢ p x✝ ∧ All p a✝ ∧ All p (b✝.append (node black l✝ v✝ r✝))

Tactic:
simp_all [hl.2.2.append hr]

Result:
no goals

Proof state:
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Tactic:
have ⟨hx, ha, hb⟩ := hl

Result:
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Proof state:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Tactic:
have := hb.append hc

Result:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (b✝.append c✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))