English
Similarly, two elements have equal right coset representations in the decomposition iff the right cosets with respect to H agree.
Русский
Аналогично, два элемента имеют равные представления правых косет в разложении тогда и только тогда, когда соответствующие правые косеты по H совпадают.
LaTeX
$$$ (\exists! h\in H, s\in S): g_i = h s \text{ for } i=1,2 \quad\text{iff}\quad \text{RightCosetEquivalence}(H,g_1,g_2). $$$
Lean4
theorem equiv_snd_eq_iff_rightCosetEquivalence {g₁ g₂ : G} :
(hHT.equiv g₁).snd = (hHT.equiv g₂).snd ↔ RightCosetEquivalence H g₁ g₂ :=
by
rw [RightCosetEquivalence, rightCoset_eq_iff]
constructor
· intro h
rw [← hHT.equiv_fst_mul_equiv_snd g₂, ← hHT.equiv_fst_mul_equiv_snd g₁, ← h, mul_inv_rev, mul_assoc,
mul_inv_cancel_left, ← coe_inv, ← coe_mul]
exact Subtype.property _
· intro h
apply (isComplement_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique
· -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
rw [equiv_snd_eq_inv_mul]; simp
· rw [SetLike.mem_coe, ← mul_mem_cancel_left h]
-- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
rw [equiv_snd_eq_inv_mul, mul_assoc]; simp
