Theorem: smallest_in_list (PnP2023/Lec_01_20/NatMin.lean)

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
by_cases c:tail = []
State after:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail

case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail

State before:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
simp [smallest, c]
State after:
no goals

State before:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
simp [smallest, c]
State after:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail

State before:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
by_cases c':head ≤ smallest tail (by simp [c])
State after:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail

case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ tail ≠ []
Tactic:
simp [c]
State after:
no goals

State before:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
left
State after:
case pos.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯

State before:
case pos.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯
Tactic:
assumption
State after:
no goals

State before:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
right
State after:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail

State before:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
have lem : 
  Nat.min head (smallest tail (by simp [c])) = smallest tail (by simp [c]) := by
    apply Nat.min_eq_right
    apply Nat.le_of_not_le 
    assumption
State after:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail

State before:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
rw [lem]
State after:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ smallest tail ⋯ ∈ tail

State before:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ smallest tail ⋯ ∈ tail
Tactic:
simp [smallest_in_list]
State after:
no goals

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ tail ≠ []
Tactic:
simp [c]
State after:
no goals

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) = smallest tail ⋯
Tactic:
apply Nat.min_eq_right
State after:
case h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ smallest tail ⋯ ≤ head

State before:
case h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ smallest tail ⋯ ≤ head
Tactic:
apply Nat.le_of_not_le
State after:
case h.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ ¬head ≤ smallest tail ⋯

State before:
case h.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ ¬head ≤ smallest tail ⋯
Tactic:
assumption
State after:
no goals