-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.WF.merge' (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) :
    (merge le s₁ s₂).WF le n ∧ ((s₁.rankGT n ↔ s₂.rankGT n) → (merge le s₁ s₂).rankGT n)

Proof state:
α✝ : Type u_1
le : α✝ → α✝ → Bool
s₁ s₂ : Heap α✝
n : Nat
h₁ : WF le n s₁
h₂ : WF le n s₂
⊢ WF le n
      (match s₁, s₂ with
      | Heap.nil, h => h
      | h, Heap.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₂)) ∧
    ((s₁.rankGT n ↔ s₂.rankGT n) →
      (match s₁, s₂ with
          | Heap.nil, h => h
          | h, Heap.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₂)).rankGT
        n)

Tactic:
split

Result:
case h_1
α✝ : Type u_1
le : α✝ → α✝ → Bool
s₂ : Heap α✝
n : Nat
h₂ : WF le n s₂
x✝¹ x✝ : Heap α✝
h₁ : WF le n Heap.nil
⊢ WF le n s₂ ∧ ((Heap.nil.rankGT n ↔ s₂.rankGT n) → s₂.rankGT n)

case h_2
α✝ : Type u_1
le : α✝ → α✝ → Bool
s₁ : Heap α✝
n : Nat
h₁ : WF le n s₁
x✝² x✝¹ : Heap α✝
x✝ : s₁ = Heap.nil → False
h₂ : WF le n Heap.nil
⊢ WF le n s₁ ∧ ((s₁.rankGT n ↔ Heap.nil.rankGT n) → s₁.rankGT n)

case h_3
α✝ : Type u_1
le : α✝ → α✝ → Bool
n : Nat
x✝¹ x✝ : Heap α✝
r₁✝ : Nat
a₁✝ : α✝
n₁✝ : HeapNode α✝
t₁✝ : Heap α✝
r₂✝ : Nat
a₂✝ : α✝
n₂✝ : HeapNode α✝
t₂✝ : Heap α✝
h₁ : WF le n (cons r₁✝ a₁✝ n₁✝ t₁✝)
h₂ : WF le n (cons r₂✝ a₂✝ n₂✝ t₂✝)
⊢ WF le n
      (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₂✝)) ∧
    (((cons r₁✝ a₁✝ n₁✝ t₁✝).rankGT n ↔ (cons r₂✝ a₂✝ n₂✝ t₂✝).rankGT n) →
      (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₂✝)).rankGT
        n)

Proof state:
case h_3.isFalse
α✝ : Type u_1
le : α✝ → α✝ → Bool
n : Nat
x✝¹ x✝ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
r₂ : Nat
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
h₁ : WF le n (cons r₁ a₁ n₁ t₁)
h₂ : WF le n (cons r₂ a₂ n₂ t₂)
hr₁ : n ≤ r₁
hn₁ : HeapNode.WF le a₁ n₁ r₁
ht₁ : WF le (r₁ + 1) t₁
hr₂ : n ≤ r₂
hn₂ : HeapNode.WF le a₂ n₂ r₂
ht₂ : WF le (r₂ + 1) t₂
lt₁ : ¬r₁ < r₂
⊢ WF le n
      (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₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n ↔ (cons r₂ a₂ n₂ t₂).rankGT n) →
      (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₂)).rankGT
        n)

Tactic:
split <;> rename_i lt₂

Result:
case h_3.isFalse.isTrue
α✝ : Type u_1
le : α✝ → α✝ → Bool
n : Nat
x✝¹ x✝ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
r₂ : Nat
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
h₁ : WF le n (cons r₁ a₁ n₁ t₁)
h₂ : WF le n (cons r₂ a₂ n₂ t₂)
hr₁ : n ≤ r₁
hn₁ : HeapNode.WF le a₁ n₁ r₁
ht₁ : WF le (r₁ + 1) t₁
hr₂ : n ≤ r₂
hn₂ : HeapNode.WF le a₂ n₂ r₂
ht₂ : WF le (r₂ + 1) t₂
lt₁ : ¬r₁ < r₂
lt₂ : r₂ < r₁
⊢ WF le n (cons r₂ a₂ n₂ (merge le (cons r₁ a₁ n₁ t₁) t₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n ↔ (cons r₂ a₂ n₂ t₂).rankGT n) →
      (cons r₂ a₂ n₂ (merge le (cons r₁ a₁ n₁ t₁) t₂)).rankGT n)

case h_3.isFalse.isFalse
α✝ : Type u_1
le : α✝ → α✝ → Bool
n : Nat
x✝¹ x✝ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
r₂ : Nat
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
h₁ : WF le n (cons r₁ a₁ n₁ t₁)
h₂ : WF le n (cons r₂ a₂ n₂ t₂)
hr₁ : n ≤ r₁
hn₁ : HeapNode.WF le a₁ n₁ r₁
ht₁ : WF le (r₁ + 1) t₁
hr₂ : n ≤ r₂
hn₂ : HeapNode.WF le a₂ n₂ r₂
ht₂ : WF le (r₂ + 1) t₂
lt₁ : ¬r₁ < r₂
lt₂ : ¬r₂ < r₁
⊢ WF le n
      (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₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n ↔ (cons r₂ a₂ n₂ t₂).rankGT n) →
      (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₂)).rankGT
        n)