Theorem: project.findMin_is_minimum_tail (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
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (findMin le [] idx (h', idx')).fst.val h'.val = true →
    ∀ (x : BinTree α), x ∈ [] → le (findMin le [] idx (h', idx')).fst.val x.val = true
Tactic:
intros _ _ hin
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' : ℕ
a✝ : le (findMin le [] idx (h', idx')).fst.val h'.val = true
x✝ : BinTree α
hin : x✝ ∈ []
⊢ le (findMin le [] idx (h', idx')).fst.val x✝.val = true

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' : ℕ
a✝ : le (findMin le [] idx (h', idx')).fst.val h'.val = true
x✝ : BinTree α
hin : x✝ ∈ []
⊢ le (findMin le [] idx (h', idx')).fst.val x✝.val = true
Tactic:
cases hin
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true →
    ∀ (x : BinTree α), x ∈ t :: ts → le (findMin le (t :: ts) idx (h', idx')).fst.val x.val = true
Tactic:
intros hle t₂ hel
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
hel : t₂ ∈ t :: ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true

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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
hel : t₂ ∈ t :: ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Tactic:
cases hel
State after:
case head
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t.val = true

case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true

State before:
case head
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t.val = true

case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Tactic:
. unfold findMin
  split
  . unfold findMin at hle
    split at hle
    . apply le_trans <;> assumption
    . contradiction
  . apply findMin_is_minimum_head <;> assumption
State after:
case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true

State before:
case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Tactic:
. unfold findMin
  split
  . unfold findMin at hle
    split at hle
    . apply findMin_is_minimum_tail <;> assumption
    . contradiction
  . apply findMin_is_minimum_tail
    . unfold findMin at hle
      split at hle
      . contradiction
      . apply findMin_is_minimum_head <;> assumption
    . assumption
State after:
no goals