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

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

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

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

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

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

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

Result:
no goals

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₁
x✝ : α✝ × HeapNode α✝
a : α✝
n : HeapNode α✝
eq : combine le a₁ a₂ n₁ n₂ = (a, n)
this : HeapNode.WF le a n (r₁ + 1)
⊢ WF le n✝
      (if t₁.rankGT (r₁ + 1) then
        if t₂.rankGT (r₁ + 1) then cons (r₁ + 1) a n (merge le t₁ t₂) else merge le (cons (r₁ + 1) a n t₁) t₂
      else if t₂.rankGT (r₁ + 1) then merge le t₁ (cons (r₁ + 1) a n t₂) else cons (r₁ + 1) a n (merge le t₁ t₂)) ∧
    (((cons r₁ a₁ n₁ t₁).rankGT n✝ ↔ (cons r₁ a₂ n₂ t₂).rankGT n✝) →
      (if t₁.rankGT (r₁ + 1) then
            if t₂.rankGT (r₁ + 1) then cons (r₁ + 1) a n (merge le t₁ t₂) else merge le (cons (r₁ + 1) a n t₁) t₂
          else
            if t₂.rankGT (r₁ + 1) then merge le t₁ (cons (r₁ + 1) a n t₂)
            else cons (r₁ + 1) a n (merge le t₁ t₂)).rankGT
        n✝)

Tactic:
split <;> split <;> rename_i hl₁ hl₂

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

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

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

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