-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Balanced.ins (cmp v) {t : RBNode α}
    (h : t.Balanced c n) : (ins cmp v t).RedRed (t.isRed = red) n

Proof state:
α : Type u_1
c : RBColor
n✝¹ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n✝ : Nat
b : RBNode α
x : α
ihr : RedRed (b.isRed = red) (ins cmp v b) n✝
x✝¹ : Ordering
heq✝ : cmp v x = Ordering.gt
n : Nat
a✝² : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
h : b.isRed = red
a✝¹ : a✝².Balanced c₁✝ n
a✝ : b✝.Balanced c₂✝ n
hl : a.Balanced black n
hr : b.Balanced black n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
⊢ RedRed ((node red a x b).isRed = red) (node red a x (node red a✝² x✝ b✝)) n

Tactic:
cases hr <;> cases h

Result:
no goals

Proof state:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
ca : RBColor
n : Nat
b : RBNode α
cb : RBColor
x : α
hl : a.Balanced ca n
hr : b.Balanced cb n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
ihr : RedRed (b.isRed = red) (ins cmp v b) n
⊢ RedRed ((node black a x b).isRed = red) (ins cmp v (node black a x b)) (n + 1)

Tactic:
unfold ins

Result:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
ca : RBColor
n : Nat
b : RBNode α
cb : RBColor
x : α
hl : a.Balanced ca n
hr : b.Balanced cb n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
ihr : RedRed (b.isRed = red) (ins cmp v b) n
⊢ RedRed ((node black a x b).isRed = red)
    (match cmp v x with
    | Ordering.lt => (ins cmp v a).balance1 x b
    | Ordering.gt => a.balance2 x (ins cmp v b)
    | Ordering.eq => node black a v b)
    (n + 1)

Proof state:
case nil
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
⊢ RedRed (nil.isRed = red) (ins cmp v nil) 0

Tactic:
exact .balanced (.red .nil .nil)

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n✝¹ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n✝ : Nat
b : RBNode α
x : α
ihr : RedRed (b.isRed = red) (ins cmp v b) n✝
x✝ : Ordering
heq✝ : cmp v x = Ordering.gt
n : Nat
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ha : l✝.Balanced black n
hb : r✝.Balanced black n
hl : a.Balanced black n
hr : b.Balanced black n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
⊢ RedRed ((node red a x b).isRed = red) (node red a x (node red l✝ v✝ r✝)) n

Tactic:
exact .redred rfl hl (.red ha hb)

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n✝¹ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
ihl : RedRed (a.isRed = red) (ins cmp v a) n
x✝ : Ordering
heq✝ : cmp v x = Ordering.lt
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
n✝ : Nat
c₁✝ c₂✝ : RBColor
ha : l✝.Balanced c₁✝ n✝
hb : r✝.Balanced c₂✝ n✝
hl : a.Balanced black (n✝ + 1)
hr : b.Balanced black (n✝ + 1)
ihr : RedRed (b.isRed = red) (ins cmp v b) (n✝ + 1)
⊢ RedRed ((node red a x b).isRed = red) (node red (node black l✝ v✝ r✝) x b) (n✝ + 1)

Tactic:
exact .balanced (.red (.black ha hb) hr)

Result:
no goals

Proof state:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
ca : RBColor
n : Nat
b : RBNode α
cb : RBColor
x : α
hl : a.Balanced ca n
hr : b.Balanced cb n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
ihr : RedRed (b.isRed = red) (ins cmp v b) n
⊢ RedRed ((node black a x b).isRed = red)
    (match cmp v x with
    | Ordering.lt => (ins cmp v a).balance1 x b
    | Ordering.gt => a.balance2 x (ins cmp v b)
    | Ordering.eq => node black a v b)
    (n + 1)

Tactic:
split

Result:
case black.h_1
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
ca : RBColor
n : Nat
b : RBNode α
cb : RBColor
x : α
hl : a.Balanced ca n
hr : b.Balanced cb n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
ihr : RedRed (b.isRed = red) (ins cmp v b) n
x✝ : Ordering
heq✝ : cmp v x = Ordering.lt
⊢ RedRed ((node black a x b).isRed = red) ((ins cmp v a).balance1 x b) (n + 1)

case black.h_2
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
ca : RBColor
n : Nat
b : RBNode α
cb : RBColor
x : α
hl : a.Balanced ca n
hr : b.Balanced cb n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
ihr : RedRed (b.isRed = red) (ins cmp v b) n
x✝ : Ordering
heq✝ : cmp v x = Ordering.gt
⊢ RedRed ((node black a x b).isRed = red) (a.balance2 x (ins cmp v b)) (n + 1)

case black.h_3
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
ca : RBColor
n : Nat
b : RBNode α
cb : RBColor
x : α
hl : a.Balanced ca n
hr : b.Balanced cb n
ihl : RedRed (a.isRed = red) (ins cmp v a) n
ihr : RedRed (b.isRed = red) (ins cmp v b) n
x✝ : Ordering
heq✝ : cmp v x = Ordering.eq
⊢ RedRed ((node black a x b).isRed = red) (node black a v b) (n + 1)

Proof state:
α : Type u_1
c : RBColor
n✝¹ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
ihr : RedRed (b.isRed = red) (ins cmp v b) n
x✝ : Ordering
heq✝ : cmp v x = Ordering.gt
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
n✝ : Nat
c₁✝ c₂✝ : RBColor
ha : l✝.Balanced c₁✝ n✝
hb : r✝.Balanced c₂✝ n✝
hl : a.Balanced black (n✝ + 1)
hr : b.Balanced black (n✝ + 1)
ihl : RedRed (a.isRed = red) (ins cmp v a) (n✝ + 1)
⊢ RedRed ((node red a x b).isRed = red) (node red a x (node black l✝ v✝ r✝)) (n✝ + 1)

Tactic:
exact .balanced (.red hl (.black ha hb))

Result:
no goals