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