-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.realSize_deleteMin {s : Heap α} (eq : s.deleteMin le = some (a, s')) :
    s.realSize = s'.realSize + 1

Proof state:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
m : Nat
ih₁ : ∀ (s : Heap α), ({ before := before, val := val, node := node, next := next }.before s).realSize = m + s.realSize
ih₂ :
  c.realSize + s.realSize + 1 =
    m + { before := before, val := val, node := node, next := next }.node.realSize +
        { before := before, val := val, node := node, next := next }.next.realSize +
      1
⊢ (cons r a c s).realSize =
    (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)).realSize +
      1

Tactic:
dsimp only at ih₁ ih₂

Result:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
m : Nat
ih₁ : ∀ (s : Heap α), (before s).realSize = m + s.realSize
ih₂ : c.realSize + s.realSize + 1 = m + node.realSize + next.realSize + 1
⊢ (cons r a c s).realSize =
    (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)).realSize +
      1

Proof state:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
m : Nat
ih₁ : ∀ (s : Heap α), (before s).realSize = m + s.realSize
ih₂ : c.realSize + s.realSize + 1 = m + node.realSize + next.realSize + 1
⊢ m + node.realSize + next.realSize + 1 =
    (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)).realSize +
      1

Tactic:
simp only [realSize_merge, HeapNode.realSize_toHeap, ih₁, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
eq : deleteMin le s = some (a, s')
⊢ s.realSize = s'.realSize + 1

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

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

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

Tactic:
have : (s.findMin le (cons r a c) ⟨id, a, c, s⟩).HasSize (c.realSize + s.realSize + 1) :=
  Heap.realSize_findMin (c.realSize + 1) (by simp) (Nat.add_right_comm ..) ⟨0, by simp⟩

Result:
case cons.refl
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
this :
  Batteries.BinomialHeap.Imp.FindMin.HasSize
    (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }) (c.realSize + s.realSize + 1)
⊢ (cons r a c s).realSize =
    (merge le (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
          ((findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
            (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next)).realSize +
      1

Proof state:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ ∀ (s : Heap α), (cons r a c s).realSize = c.realSize + 1 + s.realSize

Tactic:
simp

Result:
no goals

Proof state:
case cons.refl
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
this :
  Batteries.BinomialHeap.Imp.FindMin.HasSize
    (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }) (c.realSize + s.realSize + 1)
⊢ (cons r a c s).realSize =
    (merge le (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
          ((findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
            (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next)).realSize +
      1

Tactic:
revert this

Result:
case cons.refl
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize
      (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }) (c.realSize + s.realSize + 1) →
    (cons r a c s).realSize =
      (merge le (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
            ((findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
              (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next)).realSize +
        1

Proof state:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize { before := before, val := val, node := node, next := next }
      (c.realSize + s.realSize + 1) →
    (cons r a c s).realSize =
      (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)).realSize +
        1

Tactic:
intro ⟨m, ih₁, ih₂⟩

Result:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
m : Nat
ih₁ : ∀ (s : Heap α), ({ before := before, val := val, node := node, next := next }.before s).realSize = m + s.realSize
ih₂ :
  c.realSize + s.realSize + 1 =
    m + { before := before, val := val, node := node, next := next }.node.realSize +
        { before := before, val := val, node := node, next := next }.next.realSize +
      1
⊢ (cons r a c s).realSize =
    (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)).realSize +
      1

Proof state:
case cons.refl
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize
      (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }) (c.realSize + s.realSize + 1) →
    (cons r a c s).realSize =
      (merge le (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap
            ((findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before
              (findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next)).realSize +
        1

Tactic:
match s.findMin le (cons r a c) ⟨id, a, c, s⟩ with
| { before, val, node, next } =>
  intro ⟨m, ih₁, ih₂⟩; dsimp only at ih₁ ih₂
  rw [realSize, Nat.add_right_comm, ih₂]
  simp only [realSize_merge, HeapNode.realSize_toHeap, ih₁, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals