English
In the smulAntidiagonal context with an orderedCancelSMul, equality of the first coordinates implies equality of the second coordinates and vice versa.
Русский
В контексте smulAntidiagonal с упорядоченным аннулированием умножения равенство первых координат эквивалентно равенству вторых координат, и наоборот.
LaTeX
$$$(x: (s.\,smulAntidiagonal t a).\text{Elem}).1 = (y:(s.\,smulAntidiagonal t a).\text{Elem}).1 \iff (x).2=(y).2$$$
Lean4
@[to_additive VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd]
theorem fst_eq_fst_iff_snd_eq_snd : (x : G × P).1 = (y : G × P).1 ↔ (x : G × P).2 = (y : G × P).2 :=
⟨fun h =>
IsCancelSMul.left_cancel _ _ _
(y.2.2.2.trans <| by
rw [← h]
exact x.2.2.2.symm).symm,
fun h =>
IsCancelSMul.right_cancel _ _ _
(y.2.2.2.trans <| by
rw [← h]
exact x.2.2.2.symm).symm⟩