-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.min?_le {t : RBNode α} [TransCmp cmp] (ht : t.Ordered cmp) (h : t.min? = some a)
    (x) (hx : x ∈ t) : cmp a x ≠ .gt

Proof state:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.eq ≠ Ordering.gt

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.toList.head? = some a
x : α
hx : x ∈ t.toList
this : List.Pairwise (cmpLT cmp) t.toList
⊢ cmp a x ≠ Ordering.gt

Tactic:
revert h hx this

Result:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
⊢ t.toList.head? = some a → x ∈ t.toList → List.Pairwise (cmpLT cmp) t.toList → cmp a x ≠ Ordering.gt

Proof state:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a a ≠ Ordering.gt

Tactic:
rw [OrientedCmp.cmp_refl (cmp := cmp)]

Result:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.eq ≠ Ordering.gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
⊢ t.toList.head? = some a → x ∈ t.toList → List.Pairwise (cmpLT cmp) t.toList → cmp a x ≠ Ordering.gt

Tactic:
cases toList t <;> rintro ⟨⟩ (_ | ⟨_, hx⟩) (_ | ⟨h1,h2⟩)

Result:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a a ≠ Ordering.gt

case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a x ≠ Ordering.gt

Proof state:
case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.lt ≠ Ordering.gt

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.toList.head? = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt

Tactic:
rw [← mem_toList] at hx

Result:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.toList.head? = some a
x : α
hx : x ∈ t.toList
⊢ cmp a x ≠ Ordering.gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.min? = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt

Tactic:
rw [min?_eq_toList_head?] at h

Result:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.toList.head? = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt

Proof state:
case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a x ≠ Ordering.gt

Tactic:
rw [(h1 _ hx).1]

Result:
case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.lt ≠ Ordering.gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.toList.head? = some a
x : α
hx : x ∈ t.toList
⊢ cmp a x ≠ Ordering.gt

Tactic:
have := ht.toList_sorted

Result:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.toList.head? = some a
x : α
hx : x ∈ t.toList
this : List.Pairwise (cmpLT cmp) t.toList
⊢ cmp a x ≠ Ordering.gt