F : Type ?u.129296
α : Type u_1
β : Type ?u.129302
γ : Type ?u.129305
ι : Type ?u.129308
κ : Type ?u.129311
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x x_1 => x ⊓ x_1) ⊤ (dedup ↑l) = Multiset.inf (dedup ↑l)
F : Type ?u.129296
α : Type u_1
β : Type ?u.129302
γ : Type ?u.129305
ι : Type ?u.129308
κ : Type ?u.129311
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l = inf (List.toFinset l) id
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, inf_def, ← List.toFinset_coe, toFinset_val,
  Multiset.map_id]
no goals
F : Type ?u.129296
α : Type u_1
β : Type ?u.129302
γ : Type ?u.129305
ι : Type ?u.129308
κ : Type ?u.129311
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x x_1 => x ⊓ x_1) ⊤ (dedup ↑l) = Multiset.inf (dedup ↑l)
rfl