English
The sum of the cardinalities of the second components of the left and right transforms equals twice the cardinality of the original second component: card((mulETransformLeft e x).2) + card((mulETransformRight e x).2) = 2 * card(x.2).
Русский
Сумма кардиналов второй компоненты левого и правого преобразований равна удвоенному кардиналу исходной второй компоненты: card((mulETransformLeft e x).2) + card((mulETransformRight e x).2) = 2 * card(x.2).
LaTeX
$$$ \\operatorname{card}((\\mathrm{mulETransformLeft}\\, e\\, x).2) + \\operatorname{card}((\\mathrm{mulETransformRight}\\, e\\, x).2) = 2 \\cdot \\operatorname{card}(x.2) $$$
Lean4
@[to_additive]
theorem card : (mulETransformLeft e x).2.card + (mulETransformRight e x).2.card = 2 * x.2.card :=
(card_union_add_card_inter _ _).trans <| by rw [card_smul_finset, two_mul]
