Theorem: project.min_hRank_mergeNodes
Proof state before:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤
    hRank
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)
Tactic:
. split
  . repeat rw[hrank_of_cons]
    rw[Nat.min_eq]
    split
    . assumption
    . rfl
  . dsimp
    split
    . split
      . simp at *
        have heq : h₁.rank = h₂.rank := by
          apply Nat.le_antisymm <;> assumption
        repeat rw[hrank_of_cons]
        rw[rank_combine heq]
        rw[Nat.min_eq]
        split <;> apply Nat.le_succ
      . repeat rw[hrank_of_cons] 
        have hf : IsHeapForest' r (combine le h₁ h₂ :: t₁) := by
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          constructor
          . rw[rank_combine heq] at *
            cases ht₁
            apply Nat.lt_succ_of_lt 
            assumption
          . cases ht₁
            cases ht₂
            apply combine_IsBinTree <;> assumption
          . cases ht₁ with | cons _ _ hf =>
              rw[rank_combine heq] at *
              match hf with
              | .nil => 
                constructor
              | .cons (t := t) (ts := ts) lt _ _ =>
                constructor
                . rw[hrank_of_cons] at *
                  rename_i neq
                  unfold bne at neq
                  rw[Nat.not_beq_eq_true_eq] at neq
                  have : h₁.rank + 1 ≤  t.rank := by
                    apply Nat.succ_le_of_lt lt
                  apply lt_of_le_of_ne <;> assumption
                repeat assumption
        have hf₂ : IsHeapForest' r t₂ := by
          cases ht₂
          apply IsHeapForest'_weaken
          . assumption
          . apply Nat.le_of_lt
            assumption
        have ih := min_hRank_mergeNodes hf hf₂
        transitivity (min (hRank (combine le h₁ h₂ :: t₁)) (hRank t₂))
        . rw[hrank_of_cons] at *
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          rw[rank_combine heq] at *
          repeat rw[Nat.min_eq]
          split
          . split
            . apply Nat.le_succ
            . simp at *
              rename_i heq₂ _ hlt
              unfold bne at heq₂
              rw [Bool.not_eq_false', beq_iff_eq] at heq₂
              simp [← heq₂] at hlt 
          . split
            . apply Nat.le_succ
            . rename_i heq₂ _ hnle
              unfold bne at heq₂
              rw [Bool.not_eq_false', beq_iff_eq] at heq₂
              simp [← heq₂] at hnle
        . apply ih
    . split
      . repeat rw[hrank_of_cons]
        have hf : IsHeapForest' r t₁ := by
          cases ht₁
          apply IsHeapForest'_weaken
          . assumption
          . apply Nat.le_of_lt
            assumption
        have hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂) := by
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          constructor
          . cases ht₁
            rw[rank_combine heq] at *
            apply Nat.lt_succ_of_lt
            assumption
          . cases ht₁
            cases ht₂
            apply combine_IsBinTree <;> assumption
          . rw[rank_combine heq] at *
            cases ht₂ with | cons _ _ hf₂ =>
              match hf₂ with
              | .nil => 
                constructor
              | .cons (t := t) (ts := ts) lt _ _ => 
                rename_i hneq
                rw[hrank_of_cons] at *
                constructor
                . rw[← heq] at lt
                  unfold bne at hneq
                  rw[Nat.not_beq_eq_true_eq] at hneq
                  apply lt_of_le_of_ne <;> assumption
                repeat assumption
        have ih := min_hRank_mergeNodes hf hf₂
        transitivity (min (hRank t₁) (hRank (combine le h₁ h₂ :: t₂)))
        . rw[hrank_of_cons] at *
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          rw[rank_combine heq] at *
          repeat rw[Nat.min_eq]
          split
          . split
            . cases ht₁ with | cons _ _ hf₃ =>
                cases hf₃
                . contradiction
                . rw[hrank_of_cons]
                  apply Nat.le_of_lt
                  assumption
            . apply Nat.le_succ
          . split
            . cases ht₁ with | cons _ _ hf₃ =>
                cases hf₃
                . contradiction
                . rw[hrank_of_cons]
                  apply Nat.le_of_lt
                  assumption
            . apply Nat.le_succ
        . apply ih
      . repeat rw[hrank_of_cons]
        simp at *
        have heq : h₁.rank = h₂.rank := by
          apply Nat.le_antisymm <;> assumption
        rw[rank_combine heq]
        rw[Nat.min_eq]
        split <;> apply Nat.le_succ
Proof state after:
no goals