LeanPool.BruhatTits.Utils.List

theorem List.zipWith₃_map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {δ : Type u_7} (f : α' → β' → γ' → δ) (fa : α → α') (fb : β → β') (fc : γ → γ') (la : List α) (lb : List β) (lc : List γ) : zipWith₃ f (map fa la) (map fb lb) (map fc lc) = zipWith₃ (fun (a : α) (b : β) (c : γ) => f (fa a) (fb b) (fc c)) la lb lc