Theorem: smallest_le (Lectures/Smallest.lean)

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

State before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ head ∧
    ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Tactic:
apply And.intro
State after:
case left
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ head

case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a

State before:
case left
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ head
Tactic:
split  <;> simp
State after:
no goals

State before:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Tactic:
intro a hyp'
State after:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ a

State before:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Tactic:
have c''  := List.ne_nil_of_mem hyp'
State after:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ a

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

State before:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ head ≤ a ∨ smallest tail (_ : ¬tail = []) ≤ a
Tactic:
right
State after:
case right.h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail (_ : ¬tail = []) ≤ a

State before:
case right.h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail (_ : ¬tail = []) ≤ a
Tactic:
exact smallest_le tail c'' a hyp'
State after:
no goals