-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Ordered.ins : ∀ {path : Path α} {t : RBNode α},
    t.Ordered cmp → path.Ordered cmp → t.All (path.RootOrdered cmp) → (path.ins t).Ordered cmp
  | .root, _, ht, _, _ => Ordered.setBlack.2 ht
  | .left red parent x b, a, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
    unfold Path.ins
    have ⟨ax, ap⟩ := All_and.1 H
    exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
  | .right red a x parent, b, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
    unfold Path.ins
    have ⟨xb, bp⟩ := All_and.1 H
    exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
  | .left black parent x b, a, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
    unfold Path.ins
    have ⟨ax, ap⟩ := All_and.1 H
    exact hp.ins (ha.balance1 ax xb hb) (balance1_All.2 ⟨xp, ap, bp⟩)
  | .right black a x parent, b, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
    unfold Path.ins
    have ⟨xb, bp⟩ := All_and.1 H
    exact hp.ins (ha.balance2 ax xb hb) (balance2_All.2 ⟨xp, ap, bp⟩)

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right black a x parent)) b
xb : All (cmpLT cmp x) b
bp : All (RootOrdered cmp parent) b
⊢ RBNode.Ordered cmp (parent.ins (a.balance2 x b))

Tactic:
exact hp.ins (ha.balance2 ax xb hb) (balance2_All.2 ⟨xp, ap, bp⟩)

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left black parent x b)) a
ax : All (fun a => cmpLT cmp a x) a
ap : All (RootOrdered cmp parent) a
⊢ RBNode.Ordered cmp (parent.ins (a.balance1 x b))

Tactic:
exact hp.ins (ha.balance1 ax xb hb) (balance1_All.2 ⟨xp, ap, bp⟩)

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left black parent x b)) a
⊢ RBNode.Ordered cmp (parent.ins (a.balance1 x b))

Tactic:
have ⟨ax, ap⟩ := All_and.1 H

Result:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left black parent x b)) a
ax : All (fun a => cmpLT cmp a x) a
ap : All (RootOrdered cmp parent) a
⊢ RBNode.Ordered cmp (parent.ins (a.balance1 x b))

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right black a x parent)) b
⊢ RBNode.Ordered cmp (parent.ins (a.balance2 x b))

Tactic:
have ⟨xb, bp⟩ := All_and.1 H

Result:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right black a x parent)) b
xb : All (cmpLT cmp x) b
bp : All (RootOrdered cmp parent) b
⊢ RBNode.Ordered cmp (parent.ins (a.balance2 x b))

Proof state:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left red parent x b)) a
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Tactic:
have ⟨ax, ap⟩ := All_and.1 H

Result:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left red parent x b)) a
ax : All (fun a => cmpLT cmp a x) a
ap : All (RootOrdered cmp parent) a
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right red a x parent)) b
xb : All (cmpLT cmp x) b
bp : All (RootOrdered cmp parent) b
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Tactic:
exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right red a x parent)) b
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Tactic:
have ⟨xb, bp⟩ := All_and.1 H

Result:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right red a x parent)) b
xb : All (cmpLT cmp x) b
bp : All (RootOrdered cmp parent) b
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right black a x parent)) b
⊢ RBNode.Ordered cmp ((right black a x parent).ins b)

Tactic:
unfold Path.ins

Result:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right black a x parent)) b
⊢ RBNode.Ordered cmp (parent.ins (a.balance2 x b))

Proof state:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left black parent x b)) a
⊢ RBNode.Ordered cmp ((left black parent x b).ins a)

Tactic:
unfold Path.ins

Result:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left black parent x b)) a
⊢ RBNode.Ordered cmp (parent.ins (a.balance1 x b))