-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Balanced.append {l r : RBNode α}
    (hl : l.Balanced c₁ n) (hr : r.Balanced c₂ n) :
    (l.append r).RedRed (c₁ = black → c₂ ≠ black) n

Proof state:
case h_2
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝⁴ x✝³ a✝ : RBNode α
x✝² : α
b c : RBNode α
y✝ : α
d✝ : RBNode α
hl : (node black a✝ x✝² b).Balanced c₁ n
c₁✝¹ : RBColor
n✝ : Nat
c₂✝¹ : RBColor
ha : a✝.Balanced c₁✝¹ n✝
hb : b.Balanced c₂✝¹ n✝
hr : (node black c y✝ d✝).Balanced c₂ (n✝ + 1)
c₁✝ c₂✝ : RBColor
hc : c.Balanced c₁✝ n✝
hd : d✝.Balanced c₂✝ n✝
IH : RedRed (c₂✝¹ = black → c₁✝ ≠ black) (b.append c) n✝
l✝¹ : RBNode α
H : ∀ (a : RBNode α) (x : α) (b_1 : RBNode α), b.append c = node red a x b_1 → False
bc : RBNode α
c✝ : RBColor
hbc : bc.Balanced c✝ n✝
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), bc = node red a x b → False
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), a✝ = node red a x b → False
⊢ RedRed (black = black → black ≠ black)
    (match node black bc y✝ d✝ with
    | node black a y b => a✝.balance2 x✝² (node red a y b)
    | node red (node black a y b) z c => node red (node black a✝ x✝² a) y (b.balance2 z c.setRed)
    | r => node red a✝ x✝² r)
    (n✝ + 1)

Tactic:
exact have ⟨c, h⟩ := RedRed.balance2 ha (.redred trivial hbc hd); .balanced h

Result:
no goals

Proof state:
case h_6
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ l✝ : RBNode α
v✝ : α
r✝ : RBNode α
hr : (node black l✝ v✝ r✝).Balanced c₂ n
c₁✝ : RBColor
n✝ : Nat
c₂✝ : RBColor
hc : l✝.Balanced c₁✝ n✝
hd : r✝.Balanced c₂✝ n✝
hl : (node red a✝ x✝ b✝).Balanced c₁ (n✝ + 1)
ha : a✝.Balanced black (n✝ + 1)
hb : b✝.Balanced black (n✝ + 1)
IH✝ : RedRed (black = black → black ≠ black) (b✝.append (node black l✝ v✝ r✝)) (n✝ + 1)
c : RBColor
IH : (b✝.append (node black l✝ v✝ r✝)).Balanced c (n✝ + 1)
⊢ RedRed (red = black → black ≠ black) (node red a✝ x✝ (b✝.append (node black l✝ v✝ r✝))) (n✝ + 1)

Tactic:
exact .redred nofun ha IH

Result:
no goals

Proof state:
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b c : RBNode α
y✝ : α
d✝ : RBNode α
hl : (node black a✝ x✝ b).Balanced c₁ n
c₁✝¹ : RBColor
n✝ : Nat
c₂✝¹ : RBColor
ha : a✝.Balanced c₁✝¹ n✝
hb : b.Balanced c₂✝¹ n✝
hr : (node black c y✝ d✝).Balanced c₂ (n✝ + 1)
c₁✝ c₂✝ : RBColor
hc : c.Balanced c₁✝ n✝
hd : d✝.Balanced c₂✝ n✝
IH : RedRed (c₂✝¹ = black → c₁✝ ≠ black) (b.append c) n✝
⊢ RedRed (black = black → black ≠ black)
    (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✝))
    (n✝ + 1)

Tactic:
split

Result:
case h_1
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝³ x✝² a✝¹ : RBNode α
x✝¹ : α
b c : RBNode α
y✝ : α
d✝ : RBNode α
hl : (node black a✝¹ x✝¹ b).Balanced c₁ n
c₁✝¹ : RBColor
n✝ : Nat
c₂✝¹ : RBColor
ha : a✝¹.Balanced c₁✝¹ n✝
hb : b.Balanced c₂✝¹ n✝
hr : (node black c y✝ d✝).Balanced c₂ (n✝ + 1)
c₁✝ c₂✝ : RBColor
hc : c.Balanced c₁✝ n✝
hd : d✝.Balanced c₂✝ n✝
IH : RedRed (c₂✝¹ = black → c₁✝ ≠ black) (b.append c) n✝
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
heq✝ : b.append c = node red a✝ x✝ b✝
⊢ RedRed (black = black → black ≠ black) (node red (node black a✝¹ x✝¹ a✝) x✝ (node black b✝ y✝ d✝)) (n✝ + 1)

case h_2
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝³ x✝² a✝ : RBNode α
x✝¹ : α
b c : RBNode α
y✝ : α
d✝ : RBNode α
hl : (node black a✝ x✝¹ b).Balanced c₁ n
c₁✝¹ : RBColor
n✝ : Nat
c₂✝¹ : RBColor
ha : a✝.Balanced c₁✝¹ n✝
hb : b.Balanced c₂✝¹ n✝
hr : (node black c y✝ d✝).Balanced c₂ (n✝ + 1)
c₁✝ c₂✝ : RBColor
hc : c.Balanced c₁✝ n✝
hd : d✝.Balanced c₂✝ n✝
IH : RedRed (c₂✝¹ = black → c₁✝ ≠ black) (b.append c) n✝
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b_1 : RBNode α), b.append c = node red a x b_1 → False
⊢ RedRed (black = black → black ≠ black) (a✝.balLeft x✝¹ (node black (b.append c) y✝ d✝)) (n✝ + 1)

Proof state:
case h_6
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ l✝ : RBNode α
v✝ : α
r✝ : RBNode α
hl : (node red a✝ x✝ b✝).Balanced c₁ n
hr : (node black l✝ v✝ r✝).Balanced c₂ n
ha : a✝.Balanced black n
hb : b✝.Balanced black n
IH : RedRed (black = black → c₂ ≠ black) (b✝.append (node black l✝ v✝ r✝)) n
⊢ RedRed (red = black → c₂ ≠ black) (node red a✝ x✝ (b✝.append (node black l✝ v✝ r✝))) n

Tactic:
have .black hc hd := hr

Result:
case h_6
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ l✝ : RBNode α
v✝ : α
r✝ : RBNode α
hr : (node black l✝ v✝ r✝).Balanced c₂ n
c₁✝ : RBColor
n✝ : Nat
c₂✝ : RBColor
hc : l✝.Balanced c₁✝ n✝
hd : r✝.Balanced c₂✝ n✝
hl : (node red a✝ x✝ b✝).Balanced c₁ (n✝ + 1)
ha : a✝.Balanced black (n✝ + 1)
hb : b✝.Balanced black (n✝ + 1)
IH : RedRed (black = black → black ≠ black) (b✝.append (node black l✝ v✝ r✝)) (n✝ + 1)
⊢ RedRed (red = black → black ≠ black) (node red a✝ x✝ (b✝.append (node black l✝ v✝ r✝))) (n✝ + 1)

Proof state:
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝³ x✝² a✝ : RBNode α
x✝¹ : α
b c : RBNode α
y✝ : α
d✝ : RBNode α
hl : (node black a✝ x✝¹ b).Balanced c₁ n
c₁✝¹ : RBColor
n✝ : Nat
c₂✝¹ : RBColor
ha : a✝.Balanced c₁✝¹ n✝
hb : b.Balanced c₂✝¹ n✝
hr : (node black c y✝ d✝).Balanced c₂ (n✝ + 1)
c₁✝ c₂✝ : RBColor
hc : c.Balanced c₁✝ n✝
hd : d✝.Balanced c₂✝ n✝
IH : RedRed (c₂✝¹ = black → c₁✝ ≠ black) (b.append c) n✝
l✝ : RBNode α
H : ∀ (a : RBNode α) (x : α) (b_1 : RBNode α), b.append c = node red a x b_1 → False
bc : RBNode α
c✝ : RBColor
hbc : bc.Balanced c✝ n✝
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), bc = node red a x b → False
⊢ RedRed (black = black → black ≠ black)
    (match a✝ with
    | node red a x b => node red (node black a x b) x✝¹ (node black bc y✝ d✝)
    | l =>
      match node black bc y✝ d✝ with
      | node black a y b => l.balance2 x✝¹ (node red a y b)
      | node red (node black a y b) z c => node red (node black l x✝¹ a) y (b.balance2 z c.setRed)
      | r => node red l x✝¹ r)
    (n✝ + 1)

Tactic:
split

Result:
case h_1
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝⁴ x✝³ : RBNode α
x✝² : α
b c : RBNode α
y✝ : α
d✝ : RBNode α
c₁✝¹ : RBColor
n✝ : Nat
c₂✝¹ : RBColor
hb : b.Balanced c₂✝¹ n✝
hr : (node black c y✝ d✝).Balanced c₂ (n✝ + 1)
c₁✝ c₂✝ : RBColor
hc : c.Balanced c₁✝ n✝
hd : d✝.Balanced c₂✝ n✝
IH : RedRed (c₂✝¹ = black → c₁✝ ≠ black) (b.append c) n✝
l✝¹ : RBNode α
H : ∀ (a : RBNode α) (x : α) (b_1 : RBNode α), b.append c = node red a x b_1 → False
bc : RBNode α
c✝ : RBColor
hbc : bc.Balanced c✝ n✝
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), bc = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
hl : (node black (node red a✝ x✝ b✝) x✝² b).Balanced c₁ n
ha : (node red a✝ x✝ b✝).Balanced c₁✝¹ n✝
⊢ RedRed (black = black → black ≠ black) (node red (node black a✝ x✝ b✝) x✝² (node black bc y✝ d✝)) (n✝ + 1)

case h_2
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝⁴ x✝³ a✝ : RBNode α
x✝² : α
b c : RBNode α
y✝ : α
d✝ : RBNode α
hl : (node black a✝ x✝² b).Balanced c₁ n
c₁✝¹ : RBColor
n✝ : Nat
c₂✝¹ : RBColor
ha : a✝.Balanced c₁✝¹ n✝
hb : b.Balanced c₂✝¹ n✝
hr : (node black c y✝ d✝).Balanced c₂ (n✝ + 1)
c₁✝ c₂✝ : RBColor
hc : c.Balanced c₁✝ n✝
hd : d✝.Balanced c₂✝ n✝
IH : RedRed (c₂✝¹ = black → c₁✝ ≠ black) (b.append c) n✝
l✝¹ : RBNode α
H : ∀ (a : RBNode α) (x : α) (b_1 : RBNode α), b.append c = node red a x b_1 → False
bc : RBNode α
c✝ : RBColor
hbc : bc.Balanced c✝ n✝
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), bc = node red a x b → False
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), a✝ = node red a x b → False
⊢ RedRed (black = black → black ≠ black)
    (match node black bc y✝ d✝ with
    | node black a y b => a✝.balance2 x✝² (node red a y b)
    | node red (node black a y b) z c => node red (node black a✝ x✝² a) y (b.balance2 z c.setRed)
    | r => node red a✝ x✝² r)
    (n✝ + 1)