English
Symmetric version of triple-image commutativity: if h_comm holds for all a,b,c,d, then image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v).
Русский
Симметричное тождество для тройного образа: если выполняется равенство-правило для всех a,b,c,d, то image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v).
LaTeX
$$$\\forall a,b,c,d:\\, f(g(a,b), h(c,d)) = f'(g'(a,c), h'(b,d)) \\Rightarrow \\operatorname{image}_2 f (\\operatorname{image}_2 g s t) (\\operatorname{image}_2 h u v) = \\operatorname{image}_2 f' (\\operatorname{image}_2 g' s u) (\\operatorname{image}_2 h' t v)$$$
Lean4
theorem image2_left_comm {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε}
(h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) : image2 f s (image2 g t u) = image2 g' t (image2 f' s u) :=
by
rw [image2_swap f', image2_swap f]
exact image2_assoc fun _ _ _ => h_left_comm _ _ _
