Theorem: Imo1989P5.list_upper_bound (Compfiles/Imo1989P5.lean)

State before:
l : List ℕ
⊢ ∃ m, ∀ x ∈ l, x ≤ m
Tactic:
use List.foldr max ⊥ l
State after:
case h
l : List ℕ
⊢ ∀ x ∈ l, x ≤ List.foldr max ⊥ l

State before:
case h
l : List ℕ
⊢ ∀ x ∈ l, x ≤ List.foldr max ⊥ l
Tactic:
intro a ha
State after:
case h
l : List ℕ
a : ℕ
ha : a ∈ l
⊢ a ≤ List.foldr max ⊥ l

State before:
case h
l : List ℕ
a : ℕ
ha : a ∈ l
⊢ a ≤ List.foldr max ⊥ l
Tactic:
exact List.le_max_of_le ha (le_refl _)
State after:
no goals