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

Tactic:
cases Nat.le_antisymm (Nat.ge_of_not_lt lt₂) (Nat.ge_of_not_lt lt₁)

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

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

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

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

Tactic:
exact ⟨⟨Nat.le_succ_of_le hr₁, this, ih₁.of_rankGT (ih₂ (iff_of_false hl₁ hl₂))⟩,
  fun _ => Nat.lt_succ_of_le hr₁⟩

Result:
no goals

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

Tactic:
exact ⟨ih₁, fun _ => ih₂ ⟨fun _ => Nat.lt_succ_of_le hr₁, fun _ => ht₁.rankGT.of_le hr₁⟩⟩

Result:
no goals

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

Tactic:
exact h.2 <| Nat.lt_of_le_of_lt hr₁ lt₁

Result:
no goals

Proof state:
case 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 α✝
h : ¬le a₁ a₂ = true
⊢ HeapNode.WF le a₂ (HeapNode.node a₁ n₁ n₂) (r₁ + 1)

Tactic:
exact ⟨r₁, rfl, TotalBLE.total.resolve_left h, hn₁, hn₂⟩

Result:
no goals