F : Type ?u.664
ι : Type ?u.667
α : Type u_1
β : Type u_2
γ : Type ?u.676
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun x => f ↑x) b (List.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l)) = List.foldr f b l
F : Type ?u.664
ι : Type ?u.667
α : Type u_1
β : Type u_2
γ : Type ?u.676
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (↑l) comm b = List.foldr f b l
simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, Function.comp]
F : Type ?u.664
ι : Type ?u.667
α : Type u_1
β : Type u_2
γ : Type ?u.676
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b (List.map (fun x => ↑x) (List.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l))) = List.foldr f b l
F : Type ?u.664
ι : Type ?u.667
α : Type u_1
β : Type u_2
γ : Type ?u.676
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun x => f ↑x) b (List.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l)) = List.foldr f b l
rw [← List.foldr_map]
no goals
F : Type ?u.664
ι : Type ?u.667
α : Type u_1
β : Type u_2
γ : Type ?u.676
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b (List.map (fun x => ↑x) (List.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l))) = List.foldr f b l
simp [List.map_pmap, List.pmap_eq_map]