-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.realSize_merge (le) (s₁ s₂ : Heap α) :
    (s₁.merge le s₂).realSize = s₁.realSize + s₂.realSize

Proof state:
case isFalse.isFalse
α : Type u_1
le : α → α → Bool
x✝² x✝¹ : Heap α
r₁ : Nat
a₁ : α
n₁ : HeapNode α
t₁ : Heap α
r₂ : Nat
a₂ : α
n₂ : HeapNode α
t₂ : Heap α
IH₁ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le t₁ (cons r a n t₂)).realSize = t₁.realSize + (cons r a n t₂).realSize
IH₂ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le (cons r a n t₁) t₂).realSize = (cons r a n t₁).realSize + t₂.realSize
IH₃ : (merge le t₁ t₂).realSize = t₁.realSize + t₂.realSize
h✝¹ : ¬r₁ < r₂
h✝ : ¬r₂ < r₁
x✝ : α × HeapNode α
a✝ : α
n✝ : HeapNode α
heq✝ : combine le a₁ a₂ n₁ n₂ = (a✝, n✝)
⊢ (if t₁.rankGT (r₁ + 1) then
        if t₂.rankGT (r₁ + 1) then cons (r₁ + 1) a✝ n✝ (merge le t₁ t₂) else merge le (cons (r₁ + 1) a✝ n✝ t₁) t₂
      else
        if t₂.rankGT (r₁ + 1) then merge le t₁ (cons (r₁ + 1) a✝ n✝ t₂)
        else cons (r₁ + 1) a✝ n✝ (merge le t₁ t₂)).realSize =
    (cons r₁ a₁ n₁ t₁).realSize + (cons r₂ a₂ n₂ t₂).realSize

Tactic:
rename_i a n eq

Result:
case isFalse.isFalse
α : Type u_1
le : α → α → Bool
x✝² x✝¹ : Heap α
r₁ : Nat
a₁ : α
n₁ : HeapNode α
t₁ : Heap α
r₂ : Nat
a₂ : α
n₂ : HeapNode α
t₂ : Heap α
IH₁ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le t₁ (cons r a n t₂)).realSize = t₁.realSize + (cons r a n t₂).realSize
IH₂ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le (cons r a n t₁) t₂).realSize = (cons r a n t₁).realSize + t₂.realSize
IH₃ : (merge le t₁ t₂).realSize = t₁.realSize + t₂.realSize
h✝¹ : ¬r₁ < r₂
h✝ : ¬r₂ < r₁
x✝ : α × HeapNode α
a : α
n : HeapNode α
eq : combine le a₁ a₂ n₁ n₂ = (a, n)
⊢ (if t₁.rankGT (r₁ + 1) then
        if t₂.rankGT (r₁ + 1) then cons (r₁ + 1) a n (merge le t₁ t₂) else merge le (cons (r₁ + 1) a n t₁) t₂
      else
        if t₂.rankGT (r₁ + 1) then merge le t₁ (cons (r₁ + 1) a n t₂)
        else cons (r₁ + 1) a n (merge le t₁ t₂)).realSize =
    (cons r₁ a₁ n₁ t₁).realSize + (cons r₂ a₂ n₂ t₂).realSize

Proof state:
case isFalse.isFalse
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
r₁ : Nat
a₁ : α
n₁ : HeapNode α
t₁ : Heap α
r₂ : Nat
a₂ : α
n₂ : HeapNode α
t₂ : Heap α
IH₁ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le t₁ (cons r a n t₂)).realSize = t₁.realSize + (cons r a n t₂).realSize
IH₂ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le (cons r a n t₁) t₂).realSize = (cons r a n t₁).realSize + t₂.realSize
IH₃ : (merge le t₁ t₂).realSize = t₁.realSize + t₂.realSize
h✝¹ : ¬r₁ < r₂
h✝ : ¬r₂ < r₁
⊢ (match combine le a₁ a₂ n₁ n₂ with
      | (a, n) =>
        let r := r₁ + 1;
        if t₁.rankGT r then if t₂.rankGT r then cons r a n (merge le t₁ t₂) else merge le (cons r a n t₁) t₂
        else if t₂.rankGT r then merge le t₁ (cons r a n t₂) else cons r a n (merge le t₁ t₂)).realSize =
    (cons r₁ a₁ n₁ t₁).realSize + (cons r₂ a₂ n₂ t₂).realSize

Tactic:
split

Result:
case isFalse.isFalse
α : Type u_1
le : α → α → Bool
x✝² x✝¹ : Heap α
r₁ : Nat
a₁ : α
n₁ : HeapNode α
t₁ : Heap α
r₂ : Nat
a₂ : α
n₂ : HeapNode α
t₂ : Heap α
IH₁ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le t₁ (cons r a n t₂)).realSize = t₁.realSize + (cons r a n t₂).realSize
IH₂ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le (cons r a n t₁) t₂).realSize = (cons r a n t₁).realSize + t₂.realSize
IH₃ : (merge le t₁ t₂).realSize = t₁.realSize + t₂.realSize
h✝¹ : ¬r₁ < r₂
h✝ : ¬r₂ < r₁
x✝ : α × HeapNode α
a✝ : α
n✝ : HeapNode α
heq✝ : combine le a₁ a₂ n₁ n₂ = (a✝, n✝)
⊢ (let r := r₁ + 1;
      if t₁.rankGT r then if t₂.rankGT r then cons r a✝ n✝ (merge le t₁ t₂) else merge le (cons r a✝ n✝ t₁) t₂
      else if t₂.rankGT r then merge le t₁ (cons r a✝ n✝ t₂) else cons r a✝ n✝ (merge le t₁ t₂)).realSize =
    (cons r₁ a₁ n₁ t₁).realSize + (cons r₂ a₂ n₂ t₂).realSize

Proof state:
α : Type u_1
le : α → α → Bool
x✝² x✝¹ : Heap α
r₁ : Nat
a₁ : α
n₁ : HeapNode α
t₁ : Heap α
r₂ : Nat
a₂ : α
n₂ : HeapNode α
t₂ : Heap α
IH₁ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le t₁ (cons r a n t₂)).realSize = t₁.realSize + (cons r a n t₂).realSize
IH₂ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le (cons r a n t₁) t₂).realSize = (cons r a n t₁).realSize + t₂.realSize
IH₃ : (merge le t₁ t₂).realSize = t₁.realSize + t₂.realSize
h✝¹ : ¬r₁ < r₂
h✝ : ¬r₂ < r₁
x✝ : α × HeapNode α
a : α
n : HeapNode α
eq : (if le a₁ a₂ = true then (a₁, HeapNode.node a₂ n₂ n₁) else (a₂, HeapNode.node a₁ n₁ n₂)) = (a, n)
⊢ n.realSize = n₁.realSize + 1 + n₂.realSize

Tactic:
split at eq <;> cases eq <;>
simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
x✝² x✝¹ : Heap α
r₁ : Nat
a₁ : α
n₁ : HeapNode α
t₁ : Heap α
r₂ : Nat
a₂ : α
n₂ : HeapNode α
t₂ : Heap α
IH₁ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le t₁ (cons r a n t₂)).realSize = t₁.realSize + (cons r a n t₂).realSize
IH₂ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le (cons r a n t₁) t₂).realSize = (cons r a n t₁).realSize + t₂.realSize
IH₃ : (merge le t₁ t₂).realSize = t₁.realSize + t₂.realSize
h✝¹ : ¬r₁ < r₂
h✝ : ¬r₂ < r₁
x✝ : α × HeapNode α
a : α
n : HeapNode α
eq : combine le a₁ a₂ n₁ n₂ = (a, n)
⊢ n.realSize = n₁.realSize + 1 + n₂.realSize

Tactic:
rw [combine] at eq

Result:
α : Type u_1
le : α → α → Bool
x✝² x✝¹ : Heap α
r₁ : Nat
a₁ : α
n₁ : HeapNode α
t₁ : Heap α
r₂ : Nat
a₂ : α
n₂ : HeapNode α
t₂ : Heap α
IH₁ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le t₁ (cons r a n t₂)).realSize = t₁.realSize + (cons r a n t₂).realSize
IH₂ :
  ∀ (r : Nat) (a : α) (n : HeapNode α), (merge le (cons r a n t₁) t₂).realSize = (cons r a n t₁).realSize + t₂.realSize
IH₃ : (merge le t₁ t₂).realSize = t₁.realSize + t₂.realSize
h✝¹ : ¬r₁ < r₂
h✝ : ¬r₂ < r₁
x✝ : α × HeapNode α
a : α
n : HeapNode α
eq : (if le a₁ a₂ = true then (a₁, HeapNode.node a₂ n₂ n₁) else (a₂, HeapNode.node a₁ n₁ n₂)) = (a, n)
⊢ n.realSize = n₁.realSize + 1 + n₂.realSize

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ (match s₁, s₂ with
      | nil, h => h
      | h, nil => h
      | s₁@h:(cons r₁ a₁ n₁ t₁), s₂@h_1:(cons r₂ a₂ n₂ t₂) =>
        if r₁ < r₂ then cons r₁ a₁ n₁ (merge le t₁ s₂)
        else
          if r₂ < r₁ then cons r₂ a₂ n₂ (merge le s₁ t₂)
          else
            match combine le a₁ a₂ n₁ n₂ with
            | (a, n) =>
              let r := r₁ + 1;
              if t₁.rankGT r then if t₂.rankGT r then cons r a n (merge le t₁ t₂) else merge le (cons r a n t₁) t₂
              else if t₂.rankGT r then merge le t₁ (cons r a n t₂) else cons r a n (merge le t₁ t₂)).realSize =
    s₁.realSize + s₂.realSize

Tactic:
split

Result:
case h_1
α : Type u_1
le : α → α → Bool
s₂ x✝¹ x✝ : Heap α
⊢ s₂.realSize = nil.realSize + s₂.realSize

case h_2
α : Type u_1
le : α → α → Bool
s₁ x✝² x✝¹ : Heap α
x✝ : s₁ = nil → False
⊢ s₁.realSize = s₁.realSize + nil.realSize

case h_3
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
r₁✝ : Nat
a₁✝ : α
n₁✝ : HeapNode α
t₁✝ : Heap α
r₂✝ : Nat
a₂✝ : α
n₂✝ : HeapNode α
t₂✝ : Heap α
⊢ (if r₁✝ < r₂✝ then cons r₁✝ a₁✝ n₁✝ (merge le t₁✝ (cons r₂✝ a₂✝ n₂✝ t₂✝))
      else
        if r₂✝ < r₁✝ then cons r₂✝ a₂✝ n₂✝ (merge le (cons r₁✝ a₁✝ n₁✝ t₁✝) t₂✝)
        else
          match combine le a₁✝ a₂✝ n₁✝ n₂✝ with
          | (a, n) =>
            let r := r₁✝ + 1;
            if t₁✝.rankGT r then if t₂✝.rankGT r then cons r a n (merge le t₁✝ t₂✝) else merge le (cons r a n t₁✝) t₂✝
            else if t₂✝.rankGT r then merge le t₁✝ (cons r a n t₂✝) else cons r a n (merge le t₁✝ t₂✝)).realSize =
    (cons r₁✝ a₁✝ n₁✝ t₁✝).realSize + (cons r₂✝ a₂✝ n₂✝ t₂✝).realSize

Proof state:
case h_2
α : Type u_1
le : α → α → Bool
s₁ x✝² x✝¹ : Heap α
x✝ : s₁ = nil → False
⊢ s₁.realSize = s₁.realSize + nil.realSize

Tactic:
simp

Result:
no goals