F : Type ?u.72168
α : Type u_1
β : Type ?u.72174
γ : Type ?u.72177
ι : Type ?u.72180
κ : Type ?u.72183
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x x_1 => x ⊔ x_1) ⊥ (dedup ↑l) = Multiset.sup (dedup ↑l)
F : Type ?u.72168
α : Type u_1
β : Type ?u.72174
γ : Type ?u.72177
ι : Type ?u.72180
κ : Type ?u.72183
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l = sup (List.toFinset l) id
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, sup_def, ← List.toFinset_coe, toFinset_val,
  Multiset.map_id]
no goals
F : Type ?u.72168
α : Type u_1
β : Type ?u.72174
γ : Type ?u.72177
ι : Type ?u.72180
κ : Type ?u.72183
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x x_1 => x ⊔ x_1) ⊥ (dedup ↑l) = Multiset.sup (dedup ↑l)
rfl