-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.ins : ∀ {t : RBNode α}, t.Ordered cmp → (ins cmp x t).Ordered cmp
  | nil, _ => ⟨⟨⟩, ⟨⟩, ⟨⟩, ⟨⟩⟩
  | node red a y b, ⟨ay, yb, ha, hb⟩ => by
    unfold ins; split
    · next h => exact ⟨ay.ins ⟨h⟩, yb, ha.ins, hb⟩
    · next h => exact ⟨ay, yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩, ha, hb.ins⟩
    · next h => exact (⟨
        ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
        yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)
  | node black a y b, ⟨ay, yb, ha, hb⟩ => by
    unfold ins; split
    · next h => exact ha.ins.balance1 (ay.ins ⟨h⟩) yb hb
    · next h => exact ha.balance2 ay (yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩) hb.ins
    · next h => exact (⟨
        ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
        yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
h : cmp x y = Ordering.gt
⊢ Ordered cmp (a.balance2 y (ins cmp x b))

Tactic:
exact ha.balance2 ay (yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩) hb.ins

Result:
no goals

Proof state:
case h_3
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.eq
⊢ Ordered cmp (node red a x b)

Tactic:
next h => exact (⟨
  ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
  yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
h : cmp x y = Ordering.eq
⊢ Ordered cmp (node red a x b)

Tactic:
exact (⟨
ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
h : cmp x y = Ordering.lt
⊢ Ordered cmp ((ins cmp x a).balance1 y b)

Tactic:
exact ha.ins.balance1 (ay.ins ⟨h⟩) yb hb

Result:
no goals

Proof state:
case h_3
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.eq
⊢ Ordered cmp (node black a x b)

Tactic:
next h => exact (⟨
  ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
  yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
⊢ Ordered cmp
    (match cmp x y with
    | Ordering.lt => node red (ins cmp x a) y b
    | Ordering.gt => node red a y (ins cmp x b)
    | Ordering.eq => node red a x b)

Tactic:
split

Result:
case h_1
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.lt
⊢ Ordered cmp (node red (ins cmp x a) y b)

case h_2
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.gt
⊢ Ordered cmp (node red a y (ins cmp x b))

case h_3
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.eq
⊢ Ordered cmp (node red a x b)

Proof state:
case h_2
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.gt
⊢ Ordered cmp (a.balance2 y (ins cmp x b))

Tactic:
next h => exact ha.balance2 ay (yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩) hb.ins

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
h : cmp x y = Ordering.eq
⊢ Ordered cmp (node black a x b)

Tactic:
exact (⟨
ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)

Result:
no goals

Proof state:
case h_1
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.lt
⊢ Ordered cmp (node red (ins cmp x a) y b)

Tactic:
next h => exact ⟨ay.ins ⟨h⟩, yb, ha.ins, hb⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
⊢ Ordered cmp
    (match cmp x y with
    | Ordering.lt => (ins cmp x a).balance1 y b
    | Ordering.gt => a.balance2 y (ins cmp x b)
    | Ordering.eq => node black a x b)

Tactic:
split

Result:
case h_1
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.lt
⊢ Ordered cmp ((ins cmp x a).balance1 y b)

case h_2
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.gt
⊢ Ordered cmp (a.balance2 y (ins cmp x b))

case h_3
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.eq
⊢ Ordered cmp (node black a x b)

Proof state:
case h_2
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.gt
⊢ Ordered cmp (node red a y (ins cmp x b))

Tactic:
next h => exact ⟨ay, yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩, ha, hb.ins⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
h : cmp x y = Ordering.lt
⊢ Ordered cmp (node red (ins cmp x a) y b)

Tactic:
exact ⟨ay.ins ⟨h⟩, yb, ha.ins, hb⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
h : cmp x y = Ordering.gt
⊢ Ordered cmp (node red a y (ins cmp x b))

Tactic:
exact ⟨ay, yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩, ha, hb.ins⟩

Result:
no goals