α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
v✝ : α
r✝ x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) x✝ ∧
          All (fun x => cmpLT cmp v✝ x) r✝ ∧ RBNode.Ordered cmp x✝ ∧ RBNode.Ordered cmp r✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) x✝ ∧ All (RootOrdered cmp parent✝) r✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp v✝ x) r✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) r✝ ∧ RBNode.Ordered cmp r✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (fun x => cmpLT cmp x v✝) x✝ ∧ All (fun a => RootOrdered cmp parent✝ a) x✝
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
v✝ : α
r✝ x✝ : RBNode α
⊢ RBNode.Ordered cmp (fill (left c✝ parent✝ v✝ r✝) x✝) ↔
    Ordered cmp (left c✝ parent✝ v✝ r✝) ∧ RBNode.Ordered cmp x✝ ∧ All (RootOrdered cmp (left c✝ parent✝ v✝ r✝)) x✝
simp [Ordered.fill, RBNode.Ordered, Ordered, RootOrdered, All_and]
no goals
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
v✝ : α
r✝ x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) x✝ ∧
          All (fun x => cmpLT cmp v✝ x) r✝ ∧ RBNode.Ordered cmp x✝ ∧ RBNode.Ordered cmp r✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) x✝ ∧ All (RootOrdered cmp parent✝) r✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp v✝ x) r✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) r✝ ∧ RBNode.Ordered cmp r✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (fun x => cmpLT cmp x v✝) x✝ ∧ All (fun a => RootOrdered cmp parent✝ a) x✝
exact ⟨
  fun ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩ => ⟨⟨hp, xb, xp, bp, hb⟩, ha, ⟨ax, ap⟩⟩,
  fun ⟨⟨hp, xb, xp, bp, hb⟩, ha, ⟨ax, ap⟩⟩ => ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩⟩
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
parent✝ : Path α
x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) l✝ ∧
          All (fun x => cmpLT cmp v✝ x) x✝ ∧ RBNode.Ordered cmp l✝ ∧ RBNode.Ordered cmp x✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ All (RootOrdered cmp parent✝) x✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp x v✝) l✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ RBNode.Ordered cmp l✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (fun x => cmpLT cmp v✝ x) x✝ ∧ All (fun a => RootOrdered cmp parent✝ a) x✝
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
parent✝ : Path α
x✝ : RBNode α
⊢ RBNode.Ordered cmp (fill (right c✝ l✝ v✝ parent✝) x✝) ↔
    Ordered cmp (right c✝ l✝ v✝ parent✝) ∧ RBNode.Ordered cmp x✝ ∧ All (RootOrdered cmp (right c✝ l✝ v✝ parent✝)) x✝
simp [Ordered.fill, RBNode.Ordered, Ordered, RootOrdered, All_and]
no goals
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
parent✝ : Path α
x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) l✝ ∧
          All (fun x => cmpLT cmp v✝ x) x✝ ∧ RBNode.Ordered cmp l✝ ∧ RBNode.Ordered cmp x✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ All (RootOrdered cmp parent✝) x✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp x v✝) l✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ RBNode.Ordered cmp l✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (fun x => cmpLT cmp v✝ x) x✝ ∧ All (fun a => RootOrdered cmp parent✝ a) x✝
exact ⟨
  fun ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩ => ⟨⟨hp, ax, xp, ap, ha⟩, hb, ⟨xb, bp⟩⟩,
  fun ⟨⟨hp, ax, xp, ap, ha⟩, hb, ⟨xb, bp⟩⟩ => ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩⟩