Theorem: project.combine_IsBinTree (Project/Main.lean)

State before:
α : Type u
le : α → α → Bool
a b : BinTree α
⊢ IsBinTree a → IsBinTree b → a.rank = b.rank → IsBinTree (combine le a b)
Tactic:
intros ha hb hab
State after:
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsBinTree (combine le a b)

State before:
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsBinTree (combine le a b)
Tactic:
constructor
State after:
case a
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsRankedTree 1 (combine le a b).rank (nodes (combine le a b).children)

State before:
case a
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsRankedTree 1 (combine le a b).rank (nodes (combine le a b).children)
Tactic:
unfold combine
State after:
case a
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsRankedTree 1
    (if le b.val a.val = true then { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }
      else { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }).rank
    (nodes
      (if le b.val a.val = true then { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }
        else { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }).children)

State before:
case a
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsRankedTree 1
    (if le b.val a.val = true then { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }
      else { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }).rank
    (nodes
      (if le b.val a.val = true then { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }
        else { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }).children)
Tactic:
split
State after:
case a.«_@».Project.Main._hyg.1829.inl
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : le b.val a.val = true
⊢ IsRankedTree 1 { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.rank
    (nodes { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.children)

case a.«_@».Project.Main._hyg.1829.inr
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
⊢ IsRankedTree 1 { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.rank
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)

State before:
case a.«_@».Project.Main._hyg.1829.inl
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : le b.val a.val = true
⊢ IsRankedTree 1 { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.rank
    (nodes { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.children)

case a.«_@».Project.Main._hyg.1829.inr
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
⊢ IsRankedTree 1 { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.rank
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)
Tactic:
. dsimp
  cases hb
  apply IsRankedTree_append
  repeat assumption
State after:
case a.«_@».Project.Main._hyg.1829.inr
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
⊢ IsRankedTree 1 { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.rank
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)

State before:
case a.«_@».Project.Main._hyg.1829.inr
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
⊢ IsRankedTree 1 { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.rank
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)
Tactic:
. dsimp
  cases ha
  apply IsRankedTree_append
  repeat assumption
  simp_all
State after:
no goals

State before:
case a.«_@».Project.Main._hyg.1829.inl.mk.hrank
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hab : a.rank = b.rank
h✝ : le b.val a.val = true
a✝ : IsRankedTree 1 b.rank (nodes b.children)
⊢ a.rank = b.rank
Tactic:
assumption
State after:
no goals

State before:
case a.«_@».Project.Main._hyg.1829.inr.mk.ha
α : Type u
le : α → α → Bool
a b : BinTree α
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
a✝ : IsRankedTree 1 a.rank (nodes a.children)
⊢ IsBinTree b

case a.«_@».Project.Main._hyg.1829.inr.mk.hrank
α : Type u
le : α → α → Bool
a b : BinTree α
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
a✝ : IsRankedTree 1 a.rank (nodes a.children)
⊢ b.rank = a.rank
Tactic:
assumption
State after:
case a.«_@».Project.Main._hyg.1829.inr.mk.hrank
α : Type u
le : α → α → Bool
a b : BinTree α
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
a✝ : IsRankedTree 1 a.rank (nodes a.children)
⊢ b.rank = a.rank