Theorem: project.rank_combine (Project/Merge.lean)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
⊢ t₁.rank = t₂.rank → (combine le t₁ t₂).rank = t₁.rank + 1
Tactic:
intro
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
⊢ (combine le t₁ t₂).rank = t₁.rank + 1

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
⊢ (combine le t₁ t₂).rank = t₁.rank + 1
Tactic:
unfold combine
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
⊢ (if le t₂.val t₁.val = true then
        { val := t₂.val, rank := t₂.rank + 1, children := Heap.heap (Heap.nodes t₂.children ++ [t₁]) }
      else { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }).rank =
    t₁.rank + 1

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
⊢ (if le t₂.val t₁.val = true then
        { val := t₂.val, rank := t₂.rank + 1, children := Heap.heap (Heap.nodes t₂.children ++ [t₁]) }
      else { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }).rank =
    t₁.rank + 1
Tactic:
split
State after:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : le t₂.val t₁.val = true
⊢ { val := t₂.val, rank := t₂.rank + 1, children := Heap.heap (Heap.nodes t₂.children ++ [t₁]) }.rank = t₁.rank + 1

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : ¬le t₂.val t₁.val = true
⊢ { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }.rank = t₁.rank + 1

State before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : le t₂.val t₁.val = true
⊢ { val := t₂.val, rank := t₂.rank + 1, children := Heap.heap (Heap.nodes t₂.children ++ [t₁]) }.rank = t₁.rank + 1

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : ¬le t₂.val t₁.val = true
⊢ { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }.rank = t₁.rank + 1
Tactic:
. dsimp
  simp
  simp_all
State after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : ¬le t₂.val t₁.val = true
⊢ { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }.rank = t₁.rank + 1

State before:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : ¬le t₂.val t₁.val = true
⊢ { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }.rank = t₁.rank + 1
Tactic:
. dsimp
State after:
no goals