-- 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 root
α : Type u_1
cmp : α → α → Ordering
⊢ Ordered cmp root ↔
    List.Pairwise (cmpLT cmp) root.listL ∧
      List.Pairwise (cmpLT cmp) root.listR ∧ ∀ (x : α), x ∈ root.listL → ∀ (y : α), y ∈ root.listR → cmpLT cmp x y

Tactic:
simp

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
⊢ (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

Tactic:
exact ⟨
  fun ⟨⟨hL, hR, LR⟩, xr, ⟨Lx, xR⟩, ⟨rL, rR⟩, hr⟩ =>
    ⟨hL, ⟨⟨xr, xR⟩, hr, hR, rR⟩, Lx, fun _ ha _ hb => rL _ hb _ ha, LR⟩,
  fun ⟨hL, ⟨⟨xr, xR⟩, hr, hR, rR⟩, Lx, Lr, LR⟩ =>
    ⟨⟨hL, hR, LR⟩, xr, ⟨Lx, xR⟩, ⟨fun _ ha _ hb => Lr _ hb _ ha, rR⟩, hr⟩⟩

Result:
no goals

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
⊢ 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✝ ↔
    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:
simp [List.pairwise_append, or_imp, forall_and, ih, RBNode.ordered_iff]

Result:
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✝
⊢ (∀ (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

Tactic:
rfl

Result:
no goals

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
⊢ 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:
rw [Ordered, and_congr_right_eq fun h => by simp [All_def, rootOrdered_iff h]; rfl]

Result:
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 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✝ ↔
    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