Theorem: project.deleteMin_non_empty_minimum
Proof state before:
case h_3.inr.le_rfl
α : Type u_1
le : α → α → Bool
xs : List (HeapNodeAux α (Heap α))
y : α
ys : Heap α
t : HeapNodeAux α (Heap α)
x✝¹ : Heap α
h✝¹ : HeapNodeAux α (Heap α)
hs✝ : List (HeapNodeAux α (Heap α))
not_le_le : ∀ (x y : α), le x y = false → 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
x✝ : hs✝ = [] → False
heq✝ : xs = h✝¹ :: hs✝
heq :
  (findMin le hs✝ 1 (h✝¹, 0)).fst.val = y ∧
    merge le (Heap.heap (List.eraseIdx (h✝¹ :: hs✝) (findMin le hs✝ 1 (h✝¹, 0)).snd))
        (findMin le hs✝ 1 (h✝¹, 0)).fst.children =
      ys
h✝ : t ∈ hs✝
⊢ ∀ (z : α), le z z = true

case h_3.inr.a
α : Type u_1
le : α → α → Bool
xs : List (HeapNodeAux α (Heap α))
y : α
ys : Heap α
t : HeapNodeAux α (Heap α)
x✝¹ : Heap α
h✝¹ : HeapNodeAux α (Heap α)
hs✝ : List (HeapNodeAux α (Heap α))
not_le_le : ∀ (x y : α), le x y = false → 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
x✝ : hs✝ = [] → False
heq✝ : xs = h✝¹ :: hs✝
heq :
  (findMin le hs✝ 1 (h✝¹, 0)).fst.val = y ∧
    merge le (Heap.heap (List.eraseIdx (h✝¹ :: hs✝) (findMin le hs✝ 1 (h✝¹, 0)).snd))
        (findMin le hs✝ 1 (h✝¹, 0)).fst.children =
      ys
h✝ : t ∈ hs✝
⊢ le (findMin le hs✝ 1 (h✝¹, 0)).fst.val h✝¹.val = true

case h_3.inr.a
α : Type u_1
le : α → α → Bool
xs : List (HeapNodeAux α (Heap α))
y : α
ys : Heap α
t : HeapNodeAux α (Heap α)
x✝¹ : Heap α
h✝¹ : HeapNodeAux α (Heap α)
hs✝ : List (HeapNodeAux α (Heap α))
not_le_le : ∀ (x y : α), le x y = false → 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
x✝ : hs✝ = [] → False
heq✝ : xs = h✝¹ :: hs✝
heq :
  (findMin le hs✝ 1 (h✝¹, 0)).fst.val = y ∧
    merge le (Heap.heap (List.eraseIdx (h✝¹ :: hs✝) (findMin le hs✝ 1 (h✝¹, 0)).snd))
        (findMin le hs✝ 1 (h✝¹, 0)).fst.children =
      ys
h✝ : t ∈ hs✝
⊢ t ∈ hs✝
Tactic:
assumption
Proof state after:
case h_3.inr.a
α : Type u_1
le : α → α → Bool
xs : List (HeapNodeAux α (Heap α))
y : α
ys : Heap α
t : HeapNodeAux α (Heap α)
x✝¹ : Heap α
h✝¹ : HeapNodeAux α (Heap α)
hs✝ : List (HeapNodeAux α (Heap α))
not_le_le : ∀ (x y : α), le x y = false → 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
x✝ : hs✝ = [] → False
heq✝ : xs = h✝¹ :: hs✝
heq :
  (findMin le hs✝ 1 (h✝¹, 0)).fst.val = y ∧
    merge le (Heap.heap (List.eraseIdx (h✝¹ :: hs✝) (findMin le hs✝ 1 (h✝¹, 0)).snd))
        (findMin le hs✝ 1 (h✝¹, 0)).fst.children =
      ys
h✝ : t ∈ hs✝
⊢ le (findMin le hs✝ 1 (h✝¹, 0)).fst.val h✝¹.val = true

case h_3.inr.a
α : Type u_1
le : α → α → Bool
xs : List (HeapNodeAux α (Heap α))
y : α
ys : Heap α
t : HeapNodeAux α (Heap α)
x✝¹ : Heap α
h✝¹ : HeapNodeAux α (Heap α)
hs✝ : List (HeapNodeAux α (Heap α))
not_le_le : ∀ (x y : α), le x y = false → 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
x✝ : hs✝ = [] → False
heq✝ : xs = h✝¹ :: hs✝
heq :
  (findMin le hs✝ 1 (h✝¹, 0)).fst.val = y ∧
    merge le (Heap.heap (List.eraseIdx (h✝¹ :: hs✝) (findMin le hs✝ 1 (h✝¹, 0)).snd))
        (findMin le hs✝ 1 (h✝¹, 0)).fst.children =
      ys
h✝ : t ∈ hs✝
⊢ t ∈ hs✝