-- 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_5
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
x✝² x✝¹ l✝ : RBNode α
v✝ : α
r✝ b✝ : RBNode α
x✝ : α
c✝ : RBNode α
hl : (node black l✝ v✝ r✝).Balanced c₁ n
hr : (node red b✝ x✝ c✝).Balanced c₂ n
hc : b✝.Balanced black n
hd : c✝.Balanced black n
⊢ RedRed (c₁ = black → red ≠ black) (node red ((node black l✝ v✝ r✝).append b✝) x✝ c✝) n

Tactic:
have IH := hl.append hc

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

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
⊢ RedRed (red = black → c₂ ≠ black) (node red a✝ x✝ (b✝.append (node black l✝ v✝ r✝))) n

Tactic:
have IH := hb.append 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 α
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

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

Tactic:
have .red ha hb := hl

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

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

Tactic:
have .black ha hb := hl

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

Tactic:
have .red hc hd := hr

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

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

Tactic:
match bcc, append b c, IH, H with
| black, _, IH, _ => exact .redred nofun ha (.red IH hd)
| red, _, .red .., H => cases H _ _ _ rfl

Result:
no goals

Proof state:
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 red a✝¹ x✝¹ b).Balanced c₁ n
hr : (node red c y✝ d✝).Balanced c₂ n
ha : a✝¹.Balanced black n
hb : b.Balanced black n
hc : c.Balanced black n
hd : d✝.Balanced black n
w✝ : RBColor
IH : (b.append c).Balanced w✝ n
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
heq✝ : b.append c = node red a✝ x✝ b✝
⊢ RedRed (red = black → red ≠ black) (node red (node red a✝¹ x✝¹ a✝) x✝ (node red b✝ y✝ d✝)) n

Tactic:
next e =>
have .red hb' hc' := e ▸ IH
exact .redred nofun (.red ha hb') (.red hc' hd)

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 red a✝¹ x✝¹ b).Balanced c₁ n
hr : (node red c y✝ d✝).Balanced c₂ n
ha : a✝¹.Balanced black n
hb : b.Balanced black n
hc : c.Balanced black n
hd : d✝.Balanced black n
w✝ : RBColor
IH : (b.append c).Balanced w✝ n
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
e : b.append c = node red a✝ x✝ b✝
⊢ RedRed (red = black → red ≠ black) (node red (node red a✝¹ x✝¹ a✝) x✝ (node red b✝ y✝ d✝)) n

Tactic:
have .red hb' hc' := e ▸ IH

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

Proof state:
case h_1
α : Type u_1
c₁ : RBColor
n : Nat
c₂ : RBColor
r : RBNode α
hr : r.Balanced c₂ n
x✝¹ x✝ : RBNode α
hl : nil.Balanced c₁ n
⊢ RedRed (c₁ = black → c₂ ≠ black) r n

Tactic:
exact .balanced hr

Result:
no goals