Theorem: project.IsMinHeap_delete_BinTree (Project/DeleteMin.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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
⊢ IsMinHeap le (Heap.heap (a :: b)) → IsMinHeap le (Heap.heap (a :: List.eraseIdx b id))
Tactic:
intros imh
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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
imh : IsMinHeap le (Heap.heap (a :: b))
⊢ IsMinHeap le (Heap.heap (a :: List.eraseIdx b id))

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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
imh : IsMinHeap le (Heap.heap (a :: b))
⊢ IsMinHeap le (Heap.heap (a :: List.eraseIdx b id))
Tactic:
cases imh
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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsMinHeap le (Heap.heap (a :: List.eraseIdx b id))

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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsMinHeap le (Heap.heap (a :: List.eraseIdx b id))
Tactic:
constructor
State after:
case cons.a
α : 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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsSearchTree le a

case cons.a
α : 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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsMinHeap le (Heap.heap (List.eraseIdx b id))

State before:
case cons.a
α : 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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsSearchTree le a

case cons.a
α : 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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsMinHeap le (Heap.heap (List.eraseIdx b id))
Tactic:
. assumption
State after:
case cons.a
α : 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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsMinHeap le (Heap.heap (List.eraseIdx b id))

State before:
case cons.a
α : 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
a : HeapNodeAux α (Heap α)
b : List (HeapNodeAux α (Heap α))
id : ℕ
a✝¹ : IsSearchTree le a
a✝ : IsMinHeap le (Heap.heap b)
⊢ IsMinHeap le (Heap.heap (List.eraseIdx b id))
Tactic:
. apply IsMinHeap_eraseIdx
  assumption
State after:
no goals