-- 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:
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)

Tactic:
let ⟨hr₁, hn₁, ht₁⟩ := h₁

Result:
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₂)
hr₁ : n ≤ r₁
hn₁ : HeapNode.WF le a₁ n₁ r₁
ht₁ : WF le (r₁ + 1) 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.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₂
⊢ WF le n (cons r₁ a₁ n₁ (merge le t₁ (cons r₂ a₂ n₂ t₂))) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n ↔ (cons r₂ a₂ n₂ t₂).rankGT n) →
      (cons r₁ a₁ n₁ (merge le t₁ (cons r₂ a₂ n₂ t₂))).rankGT n)

Tactic:
refine ⟨⟨hr₁, hn₁, And.left (merge' ht₁ ⟨lt₁, hn₂, ht₂⟩)⟩, fun h => ?_⟩

Result:
case h_3.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₂
h : (cons r₁ a₁ n₁ t₁).rankGT n ↔ (cons r₂ a₂ n₂ t₂).rankGT n
⊢ (cons r₁ a₁ n₁ (merge le t₁ (cons r₂ a₂ n₂ t₂))).rankGT n

Proof state:
case h_3.isFalse.isFalse.refl.isFalse.isFalse
α✝ : Type u_1
le : α✝ → α✝ → Bool
n✝ : Nat
x✝² x✝¹ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
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₁
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₂
lt₁ lt₂ : ¬r₁ < r₁
x✝ : α✝ × HeapNode α✝
a : α✝
n : HeapNode α✝
eq : combine le a₁ a₂ n₁ n₂ = (a, n)
this : HeapNode.WF le a n (r₁ + 1)
hl₁ : ¬t₁.rankGT (r₁ + 1)
hl₂ : ¬t₂.rankGT (r₁ + 1)
⊢ WF le n✝ (cons (r₁ + 1) a n (merge le t₁ t₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n✝ ↔ (cons r₁ a₂ n₂ t₂).rankGT n✝) → (cons (r₁ + 1) a n (merge le t₁ t₂)).rankGT n✝)

Tactic:
let ⟨ih₁, ih₂⟩ := merge' ht₁ ht₂

Result:
case h_3.isFalse.isFalse.refl.isFalse.isFalse
α✝ : Type u_1
le : α✝ → α✝ → Bool
n✝ : Nat
x✝² x✝¹ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
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₁
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₂
lt₁ lt₂ : ¬r₁ < r₁
x✝ : α✝ × HeapNode α✝
a : α✝
n : HeapNode α✝
eq : combine le a₁ a₂ n₁ n₂ = (a, n)
this : HeapNode.WF le a n (r₁ + 1)
hl₁ : ¬t₁.rankGT (r₁ + 1)
hl₂ : ¬t₂.rankGT (r₁ + 1)
ih₁ : WF le (r₁ + 1) (merge le t₁ t₂)
ih₂ : (t₁.rankGT (r₁ + 1) ↔ t₂.rankGT (r₁ + 1)) → (merge le t₁ t₂).rankGT (r₁ + 1)
⊢ WF le n✝ (cons (r₁ + 1) a n (merge le t₁ t₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n✝ ↔ (cons r₁ a₂ n₂ t₂).rankGT n✝) → (cons (r₁ + 1) a n (merge le t₁ t₂)).rankGT n✝)

Proof state:
case h_3.isFalse.isFalse.refl
α✝ : Type u_1
le : α✝ → α✝ → Bool
n : Nat
x✝¹ x✝ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
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₁
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₂
lt₁ 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)

Tactic:
split

Result:
case h_3.isFalse.isFalse.refl
α✝ : Type u_1
le : α✝ → α✝ → Bool
n : Nat
x✝² x✝¹ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
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₁
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₂
lt₁ lt₂ : ¬r₁ < r₁
x✝ : α✝ × HeapNode α✝
a✝ : α✝
n✝ : HeapNode α✝
heq✝ : combine le a₁ a₂ n₁ n₂ = (a✝, n✝)
⊢ WF le 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) →
      (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)