Theorem: project.IsSearchTree_findMin (Project/findMin.lean)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsMinHeap le (Heap.heap [])
hh' : IsSearchTree le h'
⊢ IsSearchTree le (findMin le [] idx (h', idx')).fst
Tactic:
simp[findMin]
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsMinHeap le (Heap.heap [])
hh' : IsSearchTree le h'
⊢ IsSearchTree le h'

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsMinHeap le (Heap.heap [])
hh' : IsSearchTree le h'
⊢ IsSearchTree le h'
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsMinHeap le (Heap.heap (h :: hs))
hh' : IsSearchTree le h'
⊢ IsSearchTree le (findMin le (h :: hs) idx (h', idx')).fst
Tactic:
simp[findMin]
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsMinHeap le (Heap.heap (h :: hs))
hh' : IsSearchTree le h'
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsMinHeap le (Heap.heap (h :: hs))
hh' : IsSearchTree le h'
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Tactic:
cases hhs
State after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hh' : IsSearchTree le h'
a✝¹ : IsSearchTree le h
a✝ : IsMinHeap le (Heap.heap hs)
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst

State before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hh' : IsSearchTree le h'
a✝¹ : IsSearchTree le h
a✝ : IsMinHeap le (Heap.heap hs)
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Tactic:
split <;> apply IsSearchTree_findMin <;> assumption
State after:
no goals