-- 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.isFalse.isFalse.refl.isFalse.isTrue
α✝ : 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✝ (merge le t₁ (cons (r₁ + 1) a n t₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n✝ ↔ (cons r₁ a₂ n₂ t₂).rankGT n✝) → (merge le t₁ (cons (r₁ + 1) a n t₂)).rankGT n✝)

Tactic:
let ⟨ih₁, ih₂⟩ := merge' (s₂ := .cons ..) (ht₁.of_le (Nat.le_succ_of_le hr₁))
  ⟨Nat.le_succ_of_le hr₁, this, ht₂.of_rankGT hl₂⟩

Result:
case h_3.isFalse.isFalse.refl.isFalse.isTrue
α✝ : 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 n✝ (merge le t₁ (cons r₁.succ a n t₂))
ih₂ : (t₁.rankGT n✝ ↔ (cons r₁.succ a n t₂).rankGT n✝) → (merge le t₁ (cons r₁.succ a n t₂)).rankGT n✝
⊢ WF le n✝ (merge le t₁ (cons (r₁ + 1) a n t₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n✝ ↔ (cons r₁ a₂ n₂ t₂).rankGT n✝) → (merge le t₁ (cons (r₁ + 1) a n t₂)).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₂)
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₂
⊢ 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:
split <;> rename_i lt₁

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₂
⊢ 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)

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)

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

Tactic:
exact ⟨h₂, fun h => h.1 h₁⟩

Result:
no goals

Proof state:
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₁
h : (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

Tactic:
exact h.1 <| Nat.lt_of_le_of_lt hr₂ lt₂

Result:
no goals

Proof state:
case h_3.isFalse.isFalse.refl.isTrue.isTrue
α✝ : 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:
exact ⟨⟨Nat.le_succ_of_le hr₁, this,
  (merge' (ht₁.of_rankGT hl₁) (ht₂.of_rankGT hl₂)).1⟩,
  fun _ => Nat.lt_succ_of_le hr₁⟩

Result:
no goals