English
The total cardinalities across all four coordinates equal twice the total cardinality of the original pair: card((mulETransformLeft e x).1) + card((mulETransformLeft e x).2) + (card((mulETransformRight e x).1) + card((mulETransformRight e x).2)) = card(x.1) + card(x.2) + (card(x.1) + card(x.2)).
Русский
Общая сумма кардиналов всех четырех координат равна удвоенной сумме кардиналов исходной пары: card((mulETransformLeft e x).1) + card((mulETransformLeft e x).2) + (card((mulETransformRight e x).1) + card((mulETransformRight e x).2)) = card(x.1) + card(x.2) + (card(x.1) + card(x.2)).
LaTeX
$$$ \\operatorname{card}((\\mathrm{mulETransformLeft}\\, e\\, x).1) + \\operatorname{card}((\\mathrm{mulETransformLeft}\\, e\\, x).2) + \\bigl( \\operatorname{card}((\\mathrm{mulETransformRight}\\, e\\, x).1) + \\operatorname{card}((\\mathrm{mulETransformRight}\\, e\\, x).2) \\bigr) = \\operatorname{card}(x.1) + \\operatorname{card}(x.2) + (\\operatorname{card}(x.1) + \\operatorname{card}(x.2)). $$$
Lean4
/-- This statement is meant to be combined with `le_or_lt_of_add_le_add` and similar lemmas. -/
@[to_additive AddETransform.card /-- This statement is meant to be combined with
`le_or_lt_of_add_le_add` and similar lemmas. -/
]
protected theorem card :
(mulETransformLeft e x).1.card + (mulETransformLeft e x).2.card +
((mulETransformRight e x).1.card + (mulETransformRight e x).2.card) =
x.1.card + x.2.card + (x.1.card + x.2.card) :=
by rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]
