-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.WF.deleteMin {s : Heap α}
    (h : s.WF le n) (eq : s.deleteMin le = some (a, s')) : s'.WF le 0

Proof state:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
⊢ FindMin.WF le { before := before, val := val, node := node, next := next } →
    WF le 0
      (Heap.merge le { before := before, val := val, node := node, next := next }.node.toHeap
        ({ before := before, val := val, node := node, next := next }.before
          { before := before, val := val, node := node, next := next }.next))

Tactic:
intro ⟨_, hk, ih₁, ih₂⟩

Result:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
rank✝ : Nat
hk : ∀ {s : Heap α}, WF le rank✝ s → WF le 0 ({ before := before, val := val, node := node, next := next }.before s)
ih₁ :
  HeapNode.WF le { before := before, val := val, node := node, next := next }.val
    { before := before, val := val, node := node, next := next }.node rank✝
ih₂ : WF le (rank✝ + 1) { before := before, val := val, node := node, next := next }.next
⊢ WF le 0
    (Heap.merge le { before := before, val := val, node := node, next := next }.node.toHeap
      ({ before := before, val := val, node := node, next := next }.before
        { before := before, val := val, node := node, next := next }.next))

Proof state:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
⊢ FindMin.WF le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }) →
    WF le 0
      (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
        ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
          (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))

Tactic:
let { before, val, node, next } := s.findMin le (cons r a c) ⟨id, a, c, s⟩

Result:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
⊢ FindMin.WF le { before := before, val := val, node := node, next := next } →
    WF le 0
      (Heap.merge le { before := before, val := val, node := node, next := next }.node.toHeap
        ({ before := before, val := val, node := node, next := next }.before
          { before := before, val := val, node := node, next := next }.next))

Proof state:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
⊢ WF le 0
    (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
      ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))

Tactic:
have : (s.findMin le (cons r a c) ⟨id, a, c, s⟩).WF le :=
  let ⟨_, h₂, h₃⟩ := h
  h₃.findMin ⟨_, fun h => h.of_le (Nat.zero_le _), h₂, h₃⟩
    fun h => ⟨Nat.zero_le _, h₂, h⟩

Result:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
this : FindMin.WF le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
⊢ WF le 0
    (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
      ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))

Proof state:
α : Type u_1
le : α → α → Bool
n : Nat
a : α
s' s : Heap α
h : WF le n s
eq : Heap.deleteMin le s = some (a, s')
⊢ WF le 0 s'

Tactic:
cases s with cases eq | cons r a c s => ?_

Result:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
⊢ WF le 0
    (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
      ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))

Proof state:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
this : FindMin.WF le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
⊢ WF le 0
    (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
      ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))

Tactic:
revert this

Result:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
⊢ FindMin.WF le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }) →
    WF le 0
      (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
        ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
          (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))

Proof state:
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WF le n (cons r a c s)
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
rank✝ : Nat
hk : ∀ {s : Heap α}, WF le rank✝ s → WF le 0 ({ before := before, val := val, node := node, next := next }.before s)
ih₁ :
  HeapNode.WF le { before := before, val := val, node := node, next := next }.val
    { before := before, val := val, node := node, next := next }.node rank✝
ih₂ : WF le (rank✝ + 1) { before := before, val := val, node := node, next := next }.next
⊢ WF le 0
    (Heap.merge le { before := before, val := val, node := node, next := next }.node.toHeap
      ({ before := before, val := val, node := node, next := next }.before
        { before := before, val := val, node := node, next := next }.next))

Tactic:
exact ih₁.toHeap.merge <| hk (ih₂.of_le (Nat.le_succ _))

Result:
no goals