-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem isOrdered_iff' [@TransCmp α cmp] {t : RBNode α} :
    isOrdered cmp t L R ↔
    (∀ a ∈ L, t.All (cmpLT cmp a ·)) ∧
    (∀ a ∈ R, t.All (cmpLT cmp · a)) ∧
    (∀ a ∈ L, ∀ b ∈ R, cmpLT cmp a b) ∧
    Ordered cmp t

Proof state:
case nil
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
⊢ isOrdered cmp nil L R = true ↔
    (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) nil) ∧
      (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) nil) ∧
        (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp nil

Tactic:
simp [isOrdered]

Result:
case nil
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
⊢ (match L, R with
      | some l, some r => decide (cmp l r = Ordering.lt)
      | x, x_1 => true) =
      true ↔
    ∀ (a : α), L = some a → ∀ (b : α), R = some b → cmpLT cmp a b

Proof state:
case nil.h_2
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
l✝ r✝ : optParam (Option α) none
x✝ : ∀ (l r : α), L = some l → R = some r → False
⊢ ∀ (a : α), L = some a → ∀ (b : α), R = some b → cmp a b = Ordering.lt

Tactic:
next h => intro _ ha _ hb; cases h _ _ ha hb

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
l✝ r✝ : optParam (Option α) none
h : ∀ (l r : α), L = some l → R = some r → False
a✝ : α
ha : L = some a✝
b✝ : α
hb : R = some b✝
⊢ cmp a✝ b✝ = Ordering.lt

Tactic:
cases h _ _ ha hb

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
l✝ r✝ : optParam (Option α) none
h : ∀ (l r : α), L = some l → R = some r → False
⊢ ∀ (a : α), L = some a → ∀ (b : α), R = some b → cmp a b = Ordering.lt

Tactic:
intro _ ha _ hb

Result:
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
l✝ r✝ : optParam (Option α) none
h : ∀ (l r : α), L = some l → R = some r → False
a✝ : α
ha : L = some a✝
b✝ : α
hb : R = some b✝
⊢ cmp a✝ b✝ = Ordering.lt

Proof state:
case nil
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
⊢ (match L, R with
      | some l, some r => decide (cmp l r = Ordering.lt)
      | x, x_1 => true) =
      true ↔
    ∀ (a : α), L = some a → ∀ (b : α), R = some b → cmpLT cmp a b

Tactic:
split <;> simp [cmpLT_iff]

Result:
case nil.h_2
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
L R : Option α
l✝ r✝ : optParam (Option α) none
x✝ : ∀ (l r : α), L = some l → R = some r → False
⊢ ∀ (a : α), L = some a → ∀ (b : α), R = some b → cmp a b = Ordering.lt

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
c✝ : RBColor
l : RBNode α
v : α
r : RBNode α
l_ih✝ :
  ∀ {L R : Option α},
    isOrdered cmp l L R = true ↔
      (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) l) ∧
        (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) l) ∧
          (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp l
r_ih✝ :
  ∀ {L R : Option α},
    isOrdered cmp r L R = true ↔
      (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) r) ∧
        (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) r) ∧
          (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp r
L R : Option α
⊢ ((∀ (a : α), L = some a → All (fun x => cmpLT cmp a x) l) ∧
        All (fun x => cmpLT cmp x v) l ∧ (∀ (a : α), L = some a → cmpLT cmp a v) ∧ Ordered cmp l) ∧
      All (fun x => cmpLT cmp v x) r ∧
        (∀ (a : α), R = some a → All (fun x => cmpLT cmp x a) r) ∧
          (∀ (b : α), R = some b → cmpLT cmp v b) ∧ Ordered cmp r ↔
    (∀ (a : α), L = some a → cmpLT cmp a v ∧ All (fun x => cmpLT cmp a x) l ∧ All (fun x => cmpLT cmp a x) r) ∧
      (∀ (a : α), R = some a → cmpLT cmp v a ∧ All (fun x => cmpLT cmp x a) l ∧ All (fun x => cmpLT cmp x a) r) ∧
        (∀ (a : α), L = some a → ∀ (b : α), R = some b → cmpLT cmp a b) ∧
          All (fun x => cmpLT cmp x v) l ∧ All (fun x => cmpLT cmp v x) r ∧ Ordered cmp l ∧ Ordered cmp r

Tactic:
exact ⟨
  fun ⟨⟨Ll, lv, Lv, ol⟩, ⟨vr, rR, vR, or⟩⟩ => ⟨
    fun _ h => ⟨Lv _ h, Ll _ h, (Lv _ h).trans_l vr⟩,
    fun _ h => ⟨vR _ h, (vR _ h).trans_r lv, rR _ h⟩,
    fun _ hL _ hR => (Lv _ hL).trans (vR _ hR),
    lv, vr, ol, or⟩,
  fun ⟨hL, hR, _, lv, vr, ol, or⟩ => ⟨
    ⟨fun _ h => (hL _ h).2.1, lv, fun _ h => (hL _ h).1, ol⟩,
    ⟨vr, fun _ h => (hR _ h).2.2, fun _ h => (hR _ h).1, or⟩⟩⟩

Result:
no goals

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
c✝ : RBColor
l : RBNode α
v : α
r : RBNode α
l_ih✝ :
  ∀ {L R : Option α},
    isOrdered cmp l L R = true ↔
      (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) l) ∧
        (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) l) ∧
          (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp l
r_ih✝ :
  ∀ {L R : Option α},
    isOrdered cmp r L R = true ↔
      (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) r) ∧
        (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) r) ∧
          (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp r
L R : Option α
⊢ isOrdered cmp (node c✝ l v r) L R = true ↔
    (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) (node c✝ l v r)) ∧
      (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) (node c✝ l v r)) ∧
        (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp (node c✝ l v r)

Tactic:
simp [isOrdered, *]

Result:
case node
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
c✝ : RBColor
l : RBNode α
v : α
r : RBNode α
l_ih✝ :
  ∀ {L R : Option α},
    isOrdered cmp l L R = true ↔
      (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) l) ∧
        (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) l) ∧
          (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp l
r_ih✝ :
  ∀ {L R : Option α},
    isOrdered cmp r L R = true ↔
      (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) r) ∧
        (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) r) ∧
          (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp r
L R : Option α
⊢ ((∀ (a : α), L = some a → All (fun x => cmpLT cmp a x) l) ∧
        All (fun x => cmpLT cmp x v) l ∧ (∀ (a : α), L = some a → cmpLT cmp a v) ∧ Ordered cmp l) ∧
      All (fun x => cmpLT cmp v x) r ∧
        (∀ (a : α), R = some a → All (fun x => cmpLT cmp x a) r) ∧
          (∀ (b : α), R = some b → cmpLT cmp v b) ∧ Ordered cmp r ↔
    (∀ (a : α), L = some a → cmpLT cmp a v ∧ All (fun x => cmpLT cmp a x) l ∧ All (fun x => cmpLT cmp a x) r) ∧
      (∀ (a : α), R = some a → cmpLT cmp v a ∧ All (fun x => cmpLT cmp x a) l ∧ All (fun x => cmpLT cmp x a) r) ∧
        (∀ (a : α), L = some a → ∀ (b : α), R = some b → cmpLT cmp a b) ∧
          All (fun x => cmpLT cmp x v) l ∧ All (fun x => cmpLT cmp v x) r ∧ Ordered cmp l ∧ Ordered cmp r

Proof state:
α : Type u_1
cmp : α → α → Ordering
L R : Option α
inst✝ : TransCmp cmp
t : RBNode α
⊢ isOrdered cmp t L R = true ↔
    (∀ (a : α), a ∈ L → All (fun x => cmpLT cmp a x) t) ∧
      (∀ (a : α), a ∈ R → All (fun x => cmpLT cmp x a) t) ∧
        (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp t

Tactic:
induction t generalizing L R with
| nil =>
  simp [isOrdered]; split <;> simp [cmpLT_iff]
  next h => intro _ ha _ hb; cases h _ _ ha hb
| node _ l v r =>
  simp [isOrdered, *]
  exact ⟨
    fun ⟨⟨Ll, lv, Lv, ol⟩, ⟨vr, rR, vR, or⟩⟩ => ⟨
      fun _ h => ⟨Lv _ h, Ll _ h, (Lv _ h).trans_l vr⟩,
      fun _ h => ⟨vR _ h, (vR _ h).trans_r lv, rR _ h⟩,
      fun _ hL _ hR => (Lv _ hL).trans (vR _ hR),
      lv, vr, ol, or⟩,
    fun ⟨hL, hR, _, lv, vr, ol, or⟩ => ⟨
      ⟨fun _ h => (hL _ h).2.1, lv, fun _ h => (hL _ h).1, ol⟩,
      ⟨vr, fun _ h => (hR _ h).2.2, fun _ h => (hR _ h).1, or⟩⟩⟩

Result:
no goals