-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.realSize_findMin {s : Heap α}
    (m) (hk : ∀ s, (k s).realSize = m + s.realSize)
    (eq : n = m + s.realSize) (hres : res.HasSize n) :
    (s.findMin le k res).HasSize n :=
  match s with
  | .nil => hres
  | .cons r a c s => by
    simp [findMin]
    refine realSize_findMin (m + c.realSize + 1)
      (by simp [hk, Nat.add_assoc]) (by simp [eq, Nat.add_assoc]) ?_
    split
    · exact hres
    · exact ⟨m, hk, by simp [eq, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]⟩

Proof state:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
h✝ : ¬le res.val a = true
⊢ n =
    m + { before := k, val := a, node := c, next := s }.node.realSize +
        { before := k, val := a, node := c, next := s }.next.realSize +
      1

Tactic:
simp [eq, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

Result:
no goals

Proof state:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
⊢ ∀ (s : Heap α), ((k ∘ cons r a c) s).realSize = m + c.realSize + 1 + s.realSize

Tactic:
simp [hk, Nat.add_assoc]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
h✝ : le res.val a = true
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize res n

Tactic:
exact hres

Result:
no goals

Proof state:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize
    (if le res.val a = true then res else { before := k, val := a, node := c, next := s }) n

Tactic:
split

Result:
case isTrue
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
h✝ : le res.val a = true
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize res n

case isFalse
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
h✝ : ¬le res.val a = true
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize { before := k, val := a, node := c, next := s } n

Proof state:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize (findMin le k (cons r a c s) res) n

Tactic:
simp [findMin]

Result:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
⊢ Batteries.BinomialHeap.Imp.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

Proof state:
case isFalse
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
h✝ : ¬le res.val a = true
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize { before := k, val := a, node := c, next := s } n

Tactic:
exact ⟨m, hk, by simp [eq, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]⟩

Result:
no goals

Proof state:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
⊢ n = m + c.realSize + 1 + s.realSize

Tactic:
simp [eq, Nat.add_assoc]

Result:
no goals

Proof state:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
⊢ Batteries.BinomialHeap.Imp.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

Tactic:
refine realSize_findMin (m + c.realSize + 1)
  (by simp [hk, Nat.add_assoc]) (by simp [eq, Nat.add_assoc]) ?_

Result:
α : Type u_1
k : Heap α → Heap α
n : Nat
le : α → α → Bool
res : FindMin α
s✝ : Heap α
m : Nat
hk : ∀ (s : Heap α), (k s).realSize = m + s.realSize
hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n
r : Nat
a : α
c : HeapNode α
s : Heap α
eq : n = m + (cons r a c s).realSize
⊢ Batteries.BinomialHeap.Imp.FindMin.HasSize
    (if le res.val a = true then res else { before := k, val := a, node := c, next := s }) n