Theorem: smallest_mem (Lectures/Smallest.lean)

State before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
simp [smallest]
State after:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ (if c : tail = [] then head else min head (smallest tail c)) ∈ tail

State before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ (if c : tail = [] then head else min head (smallest tail c)) ∈ tail
Tactic:
split
State after:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail

case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h✝) ∈ tail

State before:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail
Tactic:
rename_i h
State after:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail

State before:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail
Tactic:
simp [h]
State after:
no goals

State before:
case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h✝) ∈ tail
Tactic:
rename_i h
State after:
case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail

State before:
case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Tactic:
by_cases h':(head ≤ smallest tail h)
State after:
case pos
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail

case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail

State before:
case pos
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Tactic:
simp [h']
State after:
no goals

State before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Tactic:
simp [h', h]
State after:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ min head (smallest tail h) ∈ tail

State before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ min head (smallest tail h) ∈ tail
Tactic:
have lem :
  min head (smallest tail h) = smallest tail h :=   by
    apply min_eq_right
    apply le_of_not_ge
    exact h'
State after:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ min head (smallest tail h) ∈ tail

State before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ min head (smallest tail h) ∈ tail
Tactic:
rw [lem]
State after:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ smallest tail h ∈ tail

State before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ smallest tail h ∈ tail
Tactic:
exact smallest_mem tail h
State after:
no goals

State before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ min head (smallest tail h) = smallest tail h
Tactic:
apply min_eq_right
State after:
case h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ smallest tail h ≤ head

State before:
case h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ smallest tail h ≤ head
Tactic:
apply le_of_not_ge
State after:
case h.a
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ ¬smallest tail h ≥ head

State before:
case h.a
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ ¬smallest tail h ≥ head
Tactic:
exact h'
State after:
no goals