English
For elements x,y of the MulAntidiagonal, equality of first coordinates implies equality of second coordinates and vice versa (under cancellation conditions).
Русский
В MulAntidiagonal равенство первых координат влечет за собой равенство вторых координат и наоборот (при некоторых условиях отмены).
LaTeX
$$Theorem: (x.1 = y.1) ↔ (x.2 = y.2) for x,y ∈ (s.mulAntidiagonal t a).Elem under commutative cancellative structure.$$
Lean4
@[to_additive Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd]
theorem fst_eq_fst_iff_snd_eq_snd : (x : α × α).1 = (y : α × α).1 ↔ (x : α × α).2 = (y : α × α).2 :=
⟨fun h =>
mul_left_cancel
(y.2.2.2.trans <| by
rw [← h]
exact x.2.2.2.symm).symm,
fun h =>
mul_right_cancel
(y.2.2.2.trans <| by
rw [← h]
exact x.2.2.2.symm).symm⟩