-- 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:
α : 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
⊢ (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

Tactic:
split

Result:
case isTrue
α : 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₂
⊢ (cons r₁ a₁ n₁ (merge le t₁ (cons r₂ a₂ n₂ t₂))).realSize = (cons r₁ a₁ n₁ t₁).realSize + (cons r₂ a₂ n₂ t₂).realSize

case 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₂
⊢ (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:
α : 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

Tactic:
have IH₁ r a n := realSize_merge le t₁ (cons r a n t₂)

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
⊢ (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:
α : 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
⊢ (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

Tactic:
have IH₃ := realSize_merge le t₁ t₂

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
⊢ (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