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

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ ∀ m ∈ head :: tail, smallest (head :: tail) hyp ≤ m
Tactic:
simp [smallest, hyp]
State after:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ head ∧
    ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a

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

case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a

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

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

State before:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Tactic:
have c'' : tail ≠ [] := by
  intro contra
  rw [contra] at hyp'
  contradiction
State after:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a

State before:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Tactic:
simp [c'']
State after:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ head ≤ a ∨ smallest tail ⋯ ≤ a

State before:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ head ≤ a ∨ smallest tail ⋯ ≤ a
Tactic:
right
State after:
case right.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail ⋯ ≤ a

State before:
case right.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail ⋯ ≤ a
Tactic:
exact smallest_le tail c'' a hyp'
State after:
no goals

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
⊢ tail ≠ []
Tactic:
intro contra
State after:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
contra : tail = []
⊢ False

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
contra : tail = []
⊢ False
Tactic:
rw [contra] at hyp'
State after:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ []
contra : tail = []
⊢ False

State before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ []
contra : tail = []
⊢ False
Tactic:
contradiction
State after:
no goals