-- 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:
case red.h_2
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
hl : a.Balanced black n
hr : b.Balanced black 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 red a x b).isRed = red) (node red a x (ins cmp v b)) n

Tactic:
match ins cmp v b, ihr with
| _, .balanced .nil => exact .balanced (.red hl .nil)
| _, .balanced (.red ha hb) => exact .redred rfl hl (.red ha hb)
| _, .balanced (.black ha hb) => exact .balanced (.red hl (.black ha hb))
| _, .redred h .. => cases hr <;> cases h

Result:
no goals

Proof state:
case red.h_3
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
hl : a.Balanced black n
hr : b.Balanced black 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 red a x b).isRed = red) (node red a v b) n

Tactic:
exact .balanced (.red hl hr)

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
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
ihr : RedRed (b.isRed = red) (ins cmp v b) n
⊢ RedRed ((node red a x b).isRed = red) (node red (node red l✝ v✝ r✝) x b) n

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

Result:
no goals

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

Tactic:
exact .balanced (.black hl hr)

Result:
no goals

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

Tactic:
exact have ⟨c, h⟩ := ihr.balance2 hl; .balanced h

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
hl : a.Balanced black 0
hr : b.Balanced black 0
ihr : RedRed (b.isRed = red) (ins cmp v b) 0
⊢ RedRed ((node red a x b).isRed = red) (node red nil x b) 0

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

Result:
no goals

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

Tactic:
exact have ⟨c, h⟩ := ihl.balance1 hr; .balanced h

Result:
no goals

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

Tactic:
split

Result:
case red.h_1
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
hl : a.Balanced black n
hr : b.Balanced black 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 red a x b).isRed = red) (node red (ins cmp v a) x b) n

case red.h_2
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
hl : a.Balanced black n
hr : b.Balanced black 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 red a x b).isRed = red) (node red a x (ins cmp v b)) n

case red.h_3
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
hl : a.Balanced black n
hr : b.Balanced black 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 red a x b).isRed = red) (node red a v b) n

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

Tactic:
unfold ins

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

Proof state:
case red.h_1
α : Type u_1
c : RBColor
n✝ : Nat
cmp : α → α → Ordering
v : α
t a : RBNode α
n : Nat
b : RBNode α
x : α
hl : a.Balanced black n
hr : b.Balanced black 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 red a x b).isRed = red) (node red (ins cmp v a) x b) n

Tactic:
match ins cmp v a, ihl with
| _, .balanced .nil => exact .balanced (.red .nil hr)
| _, .balanced (.red ha hb) => exact .redred rfl (.red ha hb) hr
| _, .balanced (.black ha hb) => exact .balanced (.red (.black ha hb) hr)
| _, .redred h .. => cases hl <;> cases h

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
hl : a.Balanced black 0
hr : b.Balanced black 0
ihl : RedRed (a.isRed = red) (ins cmp v a) 0
⊢ RedRed ((node red a x b).isRed = red) (node red a x nil) 0

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

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
n : Nat
a✝² : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
h : a.isRed = red
a✝¹ : a✝².Balanced c₁✝ n
a✝ : b✝.Balanced c₂✝ n
hl : a.Balanced black n
hr : b.Balanced black n
ihr : RedRed (b.isRed = red) (ins cmp v b) n
⊢ RedRed ((node red a x b).isRed = red) (node red (node red a✝² x✝ b✝) x b) n

Tactic:
cases hl <;> cases h

Result:
no goals