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