-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem ordered_iff {p : Path α} :
    p.Ordered cmp ↔ p.listL.Pairwise (cmpLT cmp) ∧ p.listR.Pairwise (cmpLT cmp) ∧
      ∀ x ∈ p.listL, ∀ y ∈ p.listR, cmpLT cmp x y

Proof state:
case right
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
⊢ (List.Pairwise (cmpLT cmp) parent✝.listL ∧
        List.Pairwise (cmpLT cmp) parent✝.listR ∧
          ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y) ∧
      (∀ (x_1 : α), x_1 ∈ l✝ → cmpLT cmp x_1 x) ∧
        ((∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
          ((∀ (x : α), x ∈ l✝ → ∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧
              ∀ (x : α), x ∈ l✝ → ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
            List.Pairwise (cmpLT cmp) l✝.toList ↔
    (List.Pairwise (cmpLT cmp) parent✝.listL ∧
        (List.Pairwise (cmpLT cmp) l✝.toList ∧ ∀ (a : α), a ∈ l✝ → cmpLT cmp a x) ∧
          (∀ (x : α), x ∈ parent✝.listL → ∀ (x_2 : α), x_2 ∈ l✝ → cmpLT cmp x x_2) ∧
            ∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        (∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y) ∧
          (∀ (x : α), x ∈ l✝ → ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
            ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y

Tactic:
exact ⟨
  fun ⟨⟨hL, hR, LR⟩, lx, ⟨Lx, xR⟩, ⟨lL, lR⟩, hl⟩ =>
    ⟨⟨hL, ⟨hl, lx⟩, fun _ ha _ hb => lL _ hb _ ha, Lx⟩, hR, LR, lR, xR⟩,
  fun ⟨⟨hL, ⟨hl, lx⟩, Ll, Lx⟩, hR, LR, lR, xR⟩ =>
   ⟨⟨hL, hR, LR⟩, lx, ⟨Lx, xR⟩, ⟨fun _ ha _ hb => Ll _ hb _ ha, lR⟩, hl⟩⟩

Result:
no goals

Proof state:
case left
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
x : α
r✝ : RBNode α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
⊢ Ordered cmp (left c✝ parent✝ x r✝) ↔
    List.Pairwise (cmpLT cmp) (left c✝ parent✝ x r✝).listL ∧
      List.Pairwise (cmpLT cmp) (left c✝ parent✝ x r✝).listR ∧
        ∀ (x_1 : α), x_1 ∈ (left c✝ parent✝ x r✝).listL → ∀ (y : α), y ∈ (left c✝ parent✝ x r✝).listR → cmpLT cmp x_1 y

case right
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
⊢ Ordered cmp (right c✝ l✝ x parent✝) ↔
    List.Pairwise (cmpLT cmp) (right c✝ l✝ x parent✝).listL ∧
      List.Pairwise (cmpLT cmp) (right c✝ l✝ x parent✝).listR ∧
        ∀ (x_1 : α),
          x_1 ∈ (right c✝ l✝ x parent✝).listL → ∀ (y : α), y ∈ (right c✝ l✝ x parent✝).listR → cmpLT cmp x_1 y

Tactic:
all_goals
  rw [Ordered, and_congr_right_eq fun h => by simp [All_def, rootOrdered_iff h]; rfl]
  simp [List.pairwise_append, or_imp, forall_and, ih, RBNode.ordered_iff]

Result:
case left
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
x : α
r✝ : RBNode α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
⊢ (List.Pairwise (cmpLT cmp) parent✝.listL ∧
        List.Pairwise (cmpLT cmp) parent✝.listR ∧
          ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y) ∧
      (∀ (x_1 : α), x_1 ∈ r✝ → cmpLT cmp x x_1) ∧
        ((∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
          ((∀ (x : α), x ∈ r✝ → ∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧
              ∀ (x : α), x ∈ r✝ → ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
            List.Pairwise (cmpLT cmp) r✝.toList ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      (((∀ (x_1 : α), x_1 ∈ r✝ → cmpLT cmp x x_1) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
          List.Pairwise (cmpLT cmp) r✝.toList ∧
            List.Pairwise (cmpLT cmp) parent✝.listR ∧
              ∀ (a : α), a ∈ r✝ → ∀ (b : α), b ∈ parent✝.listR → cmpLT cmp a b) ∧
        (∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧
          (∀ (x : α), x ∈ parent✝.listL → ∀ (x_2 : α), x_2 ∈ r✝ → cmpLT cmp x x_2) ∧
            ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y

case right
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
⊢ (List.Pairwise (cmpLT cmp) parent✝.listL ∧
        List.Pairwise (cmpLT cmp) parent✝.listR ∧
          ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y) ∧
      (∀ (x_1 : α), x_1 ∈ l✝ → cmpLT cmp x_1 x) ∧
        ((∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
          ((∀ (x : α), x ∈ l✝ → ∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧
              ∀ (x : α), x ∈ l✝ → ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
            List.Pairwise (cmpLT cmp) l✝.toList ↔
    (List.Pairwise (cmpLT cmp) parent✝.listL ∧
        (List.Pairwise (cmpLT cmp) l✝.toList ∧ ∀ (a : α), a ∈ l✝ → cmpLT cmp a x) ∧
          (∀ (x : α), x ∈ parent✝.listL → ∀ (x_2 : α), x_2 ∈ l✝ → cmpLT cmp x x_2) ∧
            ∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        (∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y) ∧
          (∀ (x : α), x ∈ l✝ → ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
            ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
h : Ordered cmp parent✝
⊢ (All (fun x_1 => cmpLT cmp x_1 x) l✝ ∧
      RootOrdered cmp parent✝ x ∧ All (RootOrdered cmp parent✝) l✝ ∧ RBNode.Ordered cmp l✝) =
    ?m.126878

Tactic:
simp [All_def, rootOrdered_iff h]

Result:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
h : Ordered cmp parent✝
⊢ (∀ (x_1 : α), x_1 ∈ l✝ → cmpLT cmp x_1 x) ∧
      ((∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
        (∀ (x : α),
            x ∈ l✝ → (∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a x) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp x a) ∧
          RBNode.Ordered cmp l✝ ↔
    ?m.126878