Theorem: project.IsMinHeap_eraseIdx (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
b : List (HeapNodeAux α (Heap α))
id : ℕ
⊢ IsMinHeap le (Heap.heap (List.eraseIdx [] id))
Tactic:
simp
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
b : List (HeapNodeAux α (Heap α))
id : ℕ
⊢ IsMinHeap le (Heap.heap [])

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
b : List (HeapNodeAux α (Heap α))
id : ℕ
⊢ IsMinHeap le (Heap.heap [])
Tactic:
constructor
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
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le (Heap.heap (List.eraseIdx (t :: ts) id))
Tactic:
unfold List.eraseIdx
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
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le
    (Heap.heap
      (match t :: ts, id with
      | [], x => []
      | head :: as, 0 => as
      | a :: as, Nat.succ n => a :: List.eraseIdx as n))

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
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le
    (Heap.heap
      (match t :: ts, id with
      | [], x => []
      | head :: as, 0 => as
      | a :: as, Nat.succ n => a :: List.eraseIdx as n))
Tactic:
split
State after:
case h_1
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝² : ℕ
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
heq✝ : t :: ts = []
⊢ IsMinHeap le (Heap.heap [])

case h_2
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
head✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
heq✝ : t :: ts = head✝ :: as✝
⊢ IsMinHeap le (Heap.heap as✝)

case h_3
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))

State before:
case h_1
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝² : ℕ
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
heq✝ : t :: ts = []
⊢ IsMinHeap le (Heap.heap [])

case h_2
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
head✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
heq✝ : t :: ts = head✝ :: as✝
⊢ IsMinHeap le (Heap.heap as✝)

case h_3
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))
Tactic:
. constructor
State after:
case h_2
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
head✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
heq✝ : t :: ts = head✝ :: as✝
⊢ IsMinHeap le (Heap.heap as✝)

case h_3
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))

State before:
case h_2
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
head✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
heq✝ : t :: ts = head✝ :: as✝
⊢ IsMinHeap le (Heap.heap as✝)

case h_3
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))
Tactic:
. rename_i heq
  rw[← List.tail_eq_of_cons_eq heq]
  assumption
State after:
case h_3
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))

State before:
case h_3
α : 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
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))
Tactic:
. rename_i heq
  constructor
  . rw[← List.head_eq_of_cons_eq heq]
    assumption
  . apply IsMinHeap_eraseIdx
    rw[← List.tail_eq_of_cons_eq heq]
    assumption
State after:
no goals