ext
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ univ = insert 0 (image Fin.succ univ)
case a
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
a✝ : Fin (l.length + 1)
⊢ a✝ ∈ univ ↔ a✝ ∈ insert 0 (image Fin.succ univ)