feat(group_theory/complement): API lemmas relating `range_mem_transve…

…rsals` and `to_equiv` (#13694)

This PR adds an API lemma relating `range_mem_left_transversals` (the main way of constructing left transversals) and `mem_left_transversals.to_equiv` (one of the main constructions from left transversals), and a similar lemma relating the right versions.

src/group_theory/complement.lean

@@ -241,6 +241,13 @@ noncomputable def to_equiv (hS : S ∈ subgroup.left_transversals (H : set G)) :
   quotient.mk' (to_equiv hS q : G) = q :=
 (to_equiv hS).symm_apply_apply q
 
+@[to_additive] lemma to_equiv_apply {f : G ⧸ H → G} (hf : ∀ q, (f q : G ⧸ H) = q) (q : G ⧸ H) :
+  (to_equiv (range_mem_left_transversals hf) q : G) = f q :=
+begin
+  refine (subtype.ext_iff.mp _).trans (subtype.coe_mk (f q) ⟨q, rfl⟩),
+  exact (to_equiv (range_mem_left_transversals hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm,
+end
+
 /-- A left transversal can be viewed as a function mapping each element of the group
   to the chosen representative from that left coset. -/
 @[to_additive "A left transversal can be viewed as a function mapping each element of the group
@@ -270,6 +277,14 @@ noncomputable def to_equiv (hS : S ∈ subgroup.right_transversals (H : set G))
   (q : quotient (quotient_group.right_rel H)) : quotient.mk' (to_equiv hS q : G) = q :=
 (to_equiv hS).symm_apply_apply q
 
+@[to_additive] lemma to_equiv_apply {f : quotient (quotient_group.right_rel H) → G}
+  (hf : ∀ q, quotient.mk' (f q) = q) (q : quotient (quotient_group.right_rel H)) :
+  (to_equiv (range_mem_right_transversals hf) q : G) = f q :=
+begin
+  refine (subtype.ext_iff.mp _).trans (subtype.coe_mk (f q) ⟨q, rfl⟩),
+  exact (to_equiv (range_mem_right_transversals hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm,
+end
+
 /-- A right transversal can be viewed as a function mapping each element of the group
   to the chosen representative from that right coset. -/
 @[to_additive "A right transversal can be viewed as a function mapping each element of the group