English
Twice-concatenating GenLoops along two distinct coordinates distributes: transAt i of transAt j a b and transAt j of transAt i a c equal when i ≠ j to an alternate arrangement.
Русский
Двухпорядковое конкатенирование GenLoop по разным координатам распределяется: transAt i (transAt j a b) (transAt j c d) равно transAt j (transAt i a c) (transAt i b d) при i ≠ j.
LaTeX
$$$transAt(i)(transAt(j)(a,b))(transAt(j)(c,d)) = transAt(j)(transAt(i)(a,c))(transAt(i)(b,d))$ при $i\\neq j$$$
Lean4
theorem transAt_distrib {i j : N} (h : i ≠ j) (a b c d : Ω^ N X x) :
transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d) :=
by
ext; simp_rw [transAt, coe_copy, Function.update_apply, if_neg h, if_neg h.symm]
split_ifs <;>
· congr 1; ext1; simp only [Function.update, eq_rec_constant, dite_eq_ite]
apply ite_ite_comm; rintro rfl; exact h.symm
