α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
⊢ Std.BinomialHeapImp.FindMin.HasSize
    (findMin le (k ∘ cons r a c) s
      (if le res.val a = true then res else { before := k, val := a, node := c, next := s }))
    n
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
⊢ Std.BinomialHeapImp.FindMin.HasSize (findMin le k (cons r a c s) res) n
simp [findMin]
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
⊢ Std.BinomialHeapImp.FindMin.HasSize
    (if le res.val a = true then res else { before := k, val := a, node := c, next := s }) n
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
⊢ Std.BinomialHeapImp.FindMin.HasSize
    (findMin le (k ∘ cons r a c) s
      (if le res.val a = true then res else { before := k, val := a, node := c, next := s }))
    n
refine realSize_findMin (m + c.realSize + 1)
  (by simp [hk, Nat.add_assoc]) (by simp [eq, Nat.add_assoc]) ?_
case inl
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
h✝ : le res.val a = true
⊢ Std.BinomialHeapImp.FindMin.HasSize res n

case inr
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
h✝ : ¬le res.val a = true
⊢ Std.BinomialHeapImp.FindMin.HasSize { before := k, val := a, node := c, next := s } n
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
⊢ Std.BinomialHeapImp.FindMin.HasSize
    (if le res.val a = true then res else { before := k, val := a, node := c, next := s }) n
split
case inr
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
h✝ : ¬le res.val a = true
⊢ Std.BinomialHeapImp.FindMin.HasSize { before := k, val := a, node := c, next := s } n
case inl
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
h✝ : le res.val a = true
⊢ Std.BinomialHeapImp.FindMin.HasSize res n

case inr
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
h✝ : ¬le res.val a = true
⊢ Std.BinomialHeapImp.FindMin.HasSize { before := k, val := a, node := c, next := s } n
{ exact hres }
no goals
case inr
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
h✝ : ¬le res.val a = true
⊢ Std.BinomialHeapImp.FindMin.HasSize { before := k, val := a, node := c, next := s } n
exact ⟨m, hk, by simp [eq, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]⟩
no goals
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
⊢ ∀ (s : Heap α), realSize ((k ∘ cons r a c) s) = m + HeapNode.realSize c + 1 + realSize s
simp [hk, Nat.add_assoc]
no goals
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
⊢ n = m + HeapNode.realSize c + 1 + realSize s
simp [eq, Nat.add_assoc]
no goals
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), realSize (k s) = m + realSize s
hres : Std.BinomialHeapImp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + realSize (cons r a c s)
h✝ : ¬le res.val a = true
⊢ n =
    m + HeapNode.realSize { before := k, val := a, node := c, next := s }.node +
        realSize { before := k, val := a, node := c, next := s }.next +
      1
simp [eq, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]