rintro (rfl | h)
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
case cons.inl
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
ih : a ∈ l → a ≤ l.sup
⊢ a ≤ a ⊔ l.sup

case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup