internlm/Lean-Github huggingface dataset:
Theorem: project.combine_IsBinTree
Proof 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
Proof 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)
Theorem: project.combine_IsBinTree
Proof 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
Proof 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)
Theorem: project.combine_IsBinTree
Proof 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
Proof 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)
Theorem: project.combine_IsBinTree
Proof 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
Proof 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)
Theorem: project.combine_IsBinTree
Proof 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
Proof 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)
Theorem: project.combine_IsBinTree
Proof 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
Proof state after:
no goals
Theorem: project.combine_IsBinTree
Proof 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
Proof state after:
no goals
Theorem: project.combine_IsBinTree
Proof 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
Proof 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
Theorem: project.IsMinTree_append
Proof state before:
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
xs : List (BinTree α✝)
a : BinTree α✝
h : IsMinTree le m xs
ha : IsSearchTree le a
hba : le m a.val = true
⊢ IsMinTree le m (xs ++ [a])
Tactic:
induction xs with
| nil =>
  simp
  constructor <;> assumption
| cons _ _ ih => 
  cases h
  constructor
  . assumption
  . simp
    apply ih
    assumption
  . assumption
Proof state after:
no goals
Theorem: project.IsMinTree_append
Proof state before:
case nil
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
h : IsMinTree le m []
⊢ IsMinTree le m ([] ++ [a])
Tactic:
simp
Proof state after:
case nil
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
h : IsMinTree le m []
⊢ IsMinTree le m [a]
Theorem: project.IsMinTree_append
Proof state before:
case nil
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
h : IsMinTree le m []
⊢ IsMinTree le m [a]
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: project.IsMinTree_append
Proof state before:
case cons
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
h : IsMinTree le m (head✝ :: tail✝)
⊢ IsMinTree le m (head✝ :: tail✝ ++ [a])
Tactic:
cases h
Proof state after:
case cons.cons
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (head✝ :: tail✝ ++ [a])
Theorem: project.IsMinTree_append
Proof state before:
case cons.cons
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (head✝ :: tail✝ ++ [a])
Tactic:
constructor
Proof state after:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ le m head✝.val = true

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Theorem: project.IsMinTree_append
Proof state before:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ le m head✝.val = true

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Tactic:
. assumption
Proof state after:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Theorem: project.IsMinTree_append
Proof state before:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Tactic:
. simp
  apply ih
  assumption
Proof state after:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Theorem: project.IsMinTree_append
Proof state before:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Tactic:
. assumption
Proof state after:
no goals
Theorem: project.combine_IsSearchTree
Proof 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
Proof 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)
Theorem: project.combine_IsSearchTree
Proof 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
Proof 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)
Theorem: project.combine_IsSearchTree
Proof 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
Proof 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)
Theorem: project.combine_IsSearchTree
Proof 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
Proof 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)
Theorem: project.combine_IsSearchTree
Proof 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
Proof 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)
Theorem: project.combine_IsSearchTree
Proof 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
Proof state after:
no goals
Theorem: project.combine_IsSearchTree
Proof 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
Proof state after:
no goals
Theorem: project.combine_IsSearchTree
Proof 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
Proof 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
Theorem: project.IsBinTree_findMin
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsHeapForest' r []
hh' : IsBinTree h'
⊢ IsBinTree (findMin le [] idx (h', idx')).fst
Tactic:
simp[findMin]
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsHeapForest' r []
hh' : IsBinTree h'
⊢ IsBinTree h'
Theorem: project.IsBinTree_findMin
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsHeapForest' r []
hh' : IsBinTree h'
⊢ IsBinTree h'
Tactic:
assumption
Proof state after:
no goals
Theorem: project.IsBinTree_findMin
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
h : BinTree α
hs : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsHeapForest' r (h :: hs)
hh' : IsBinTree h'
⊢ IsBinTree (findMin le (h :: hs) idx (h', idx')).fst
Tactic:
simp[findMin]
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
h : BinTree α
hs : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsHeapForest' r (h :: hs)
hh' : IsBinTree h'
⊢ IsBinTree
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Theorem: project.IsBinTree_findMin
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
h : BinTree α
hs : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsHeapForest' r (h :: hs)
hh' : IsBinTree h'
⊢ IsBinTree
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Tactic:
cases hhs
Proof state after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
h : BinTree α
hs : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hh' : IsBinTree h'
a✝² : IsBinTree h
a✝¹ : r < h.rank
a✝ : IsHeapForest' h.rank hs
⊢ IsBinTree
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Theorem: project.IsBinTree_findMin
Proof state before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
h : BinTree α
hs : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hh' : IsBinTree h'
a✝² : IsBinTree h
a✝¹ : r < h.rank
a✝ : IsHeapForest' h.rank hs
⊢ IsBinTree
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Tactic:
split <;> apply IsBinTree_findMin <;> assumption
Proof state after:
no goals
Theorem: project.IsSearchTree_findMin
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsMinHeap le (Heap.heap [])
hh' : IsSearchTree le h'
⊢ IsSearchTree le (findMin le [] idx (h', idx')).fst
Tactic:
simp[findMin]
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsMinHeap le (Heap.heap [])
hh' : IsSearchTree le h'
⊢ IsSearchTree le h'
Theorem: project.IsSearchTree_findMin
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
idx : ℕ
h' : BinTree α
idx' : ℕ
x✝ : IsMinHeap le (Heap.heap [])
hh' : IsSearchTree le h'
⊢ IsSearchTree le h'
Tactic:
assumption
Proof state after:
no goals