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

State before:
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
⊢ IsSearchTree le a → IsSearchTree le b → IsSearchTree le (combine le a b)
Tactic:
intros ha hb
State after:
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
⊢ IsSearchTree le (combine le a b)

State before:
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
⊢ IsSearchTree le (combine le a b)
Tactic:
constructor
State after:
case a
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
⊢ IsMinTree le (combine le a b).val (nodes (combine le a b).children)

State before:
case a
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
⊢ IsMinTree le (combine le a b).val (nodes (combine le a b).children)
Tactic:
unfold combine
State after:
case a
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
⊢ IsMinTree le
    (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]) }).val
    (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
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
⊢ IsMinTree le
    (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]) }).val
    (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.2095.inl
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : le b.val a.val = true
⊢ IsMinTree le { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.val
    (nodes { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.children)

case a.«_@».Project.Main._hyg.2095.inr
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
⊢ IsMinTree le { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.val
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)

State before:
case a.«_@».Project.Main._hyg.2095.inl
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : le b.val a.val = true
⊢ IsMinTree le { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.val
    (nodes { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.children)

case a.«_@».Project.Main._hyg.2095.inr
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
⊢ IsMinTree le { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.val
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)
Tactic:
. dsimp
  cases hb
  apply IsMinTree_append
  repeat assumption
State after:
case a.«_@».Project.Main._hyg.2095.inr
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
⊢ IsMinTree le { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.val
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)

State before:
case a.«_@».Project.Main._hyg.2095.inr
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
⊢ IsMinTree le { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.val
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)
Tactic:
. dsimp
  cases ha
  apply IsMinTree_append
  repeat assumption
  apply not_le_le
  assumption
State after:
no goals

State before:
case a.«_@».Project.Main._hyg.2095.inl.mk.hba
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
h✝ : le b.val a.val = true
a✝ : IsMinTree le b.val (nodes b.children)
⊢ le b.val a.val = true
Tactic:
assumption
State after:
no goals

State before:
case a.«_@».Project.Main._hyg.2095.inr.mk.ha
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
a✝ : IsMinTree le a.val (nodes a.children)
⊢ IsSearchTree le b

case a.«_@».Project.Main._hyg.2095.inr.mk.hba
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
a✝ : IsMinTree le a.val (nodes a.children)
⊢ le a.val b.val = true
Tactic:
assumption
State after:
case a.«_@».Project.Main._hyg.2095.inr.mk.hba
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
a✝ : IsMinTree le a.val (nodes a.children)
⊢ le a.val b.val = true