Theorem: Std.RBNode.Ordered.min?_le (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : RBNode.min? t = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt
Tactic:
rw [min?_eq_toList_head?] at h
State after:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt

State before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt
Tactic:
rw [← mem_toList] at hx
State after:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ toList t
⊢ cmp a x ≠ Ordering.gt

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

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

State before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
⊢ List.head? (toList t) = some a → x ∈ toList t → List.Pairwise (cmpLT cmp) (toList t) → cmp a x ≠ Ordering.gt
Tactic:
cases toList t <;> rintro ⟨⟩ (_ | ⟨_, hx⟩) (_ | ⟨h1,h2⟩)
State after:
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

State before:
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)]
State after:
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

State before:
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
State after:
no goals

State before:
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]
State after:
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

State before:
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
State after:
no goals