no goals
F : Type ?u.3706
ι : Type ?u.3709
α : Type u_1
β : Type ?u.3715
γ : Type ?u.3718
f : α → β → β
op : α → α → α
assoc : IsAssociative α op
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => op x y = op y x
a : α
⊢ noncommFold op (↑l) comm a = List.foldr op a l
simp [noncommFold]