induction' l with a l ih <;> simp[*]
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
⊢ a ∈ l → a ≤ l.sup
case cons
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
⊢ a✝ = a ∨ a✝ ∈ l → a✝ ≤ a ⊔ l.sup