Theorem: project.IsBinTree_findMin (Project/findMin.lean)

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]
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'

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
State after:
no goals

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]
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

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
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

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
State after:
no goals