feat(group_theory/coset): Add quotient_equiv_of_eq (#16439)

This PR adds `quotient_equiv_of_eq` and renames `equiv_quotient_of_eq` to `quotient_mul_equiv_of_eq`.

Author: tb65536

src/data/zmod/quotient.lean

@@ -39,13 +39,13 @@ namespace int
 /-- `ℤ` modulo multiples of `n : ℕ` is `zmod n`. -/
 def quotient_zmultiples_nat_equiv_zmod :
   ℤ ⧸ add_subgroup.zmultiples (n : ℤ) ≃+ zmod n :=
-(equiv_quotient_of_eq (zmod.ker_int_cast_add_hom _)).symm.trans $
+(quotient_add_equiv_of_eq (zmod.ker_int_cast_add_hom _)).symm.trans $
 quotient_ker_equiv_of_right_inverse (int.cast_add_hom (zmod n)) coe int_cast_zmod_cast
 
 /-- `ℤ` modulo multiples of `a : ℤ` is `zmod a.nat_abs`. -/
 def quotient_zmultiples_equiv_zmod (a : ℤ) :
   ℤ ⧸ add_subgroup.zmultiples a ≃+ zmod a.nat_abs :=
-(equiv_quotient_of_eq (zmultiples_nat_abs a)).symm.trans
+(quotient_add_equiv_of_eq (zmultiples_nat_abs a)).symm.trans
   (quotient_zmultiples_nat_equiv_zmod a.nat_abs)
 
 /-- `ℤ` modulo the ideal generated by `n : ℕ` is `zmod n`. -/

src/group_theory/coset.lean

@@ -441,6 +441,18 @@ calc α ≃ Σ L : α ⧸ s, {x : α // (x : α ⧸ s) = L} :
 
 variables {t : subgroup α}
 
+/-- If two subgroups `M` and `N` of `G` are equal, their quotients are in bijection. -/
+@[to_additive "If two subgroups `M` and `N` of `G` are equal, their quotients are in bijection."]
+def quotient_equiv_of_eq (h : s = t) : α ⧸ s ≃ α ⧸ t :=
+{ to_fun := quotient.map' id (λ a b h', h ▸ h'),
+  inv_fun := quotient.map' id (λ a b h', h.symm ▸ h'),
+  left_inv := λ q, induction_on' q (λ g, rfl),
+  right_inv := λ q, induction_on' q (λ g, rfl) }
+
+lemma quotient_equiv_of_eq_mk (h : s = t) (a : α) :
+  quotient_equiv_of_eq h (quotient_group.mk a) = (quotient_group.mk a) :=
+rfl
+
 /-- If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse
 of the quotient map `G → G/K`. The classical version is `quotient_equiv_prod_of_le`. -/
 @[to_additive "If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse

src/group_theory/quotient_group.lean

@@ -275,17 +275,14 @@ quotient_ker_equiv_of_right_inverse φ _ hφ.has_right_inverse.some_spec
 isomorphic. -/
 @[to_additive "If two normal subgroups `M` and `N` of `G` are the same, their quotient groups are
 isomorphic."]
-def equiv_quotient_of_eq {M N : subgroup G} [M.normal] [N.normal] (h : M = N) :
+def quotient_mul_equiv_of_eq {M N : subgroup G} [M.normal] [N.normal] (h : M = N) :
   G ⧸ M ≃* G ⧸ N :=
-{ to_fun := (lift M (mk' N) (λ m hm, quotient_group.eq.mpr (by simpa [← h] using M.inv_mem hm))),
-  inv_fun := (lift N (mk' M) (λ n hn, quotient_group.eq.mpr (by simpa [← h] using N.inv_mem hn))),
-  left_inv := λ x, x.induction_on' $ by { intro, refl },
-  right_inv := λ x, x.induction_on' $ by { intro, refl },
-  map_mul' := λ x y, by rw monoid_hom.map_mul }
+{ map_mul' := λ q r, quotient.induction_on₂' q r (λ g h, rfl),
+  .. subgroup.quotient_equiv_of_eq h }
 
 @[simp, to_additive]
-lemma equiv_quotient_of_eq_mk {M N : subgroup G} [M.normal] [N.normal] (h : M = N) (x : G) :
-  quotient_group.equiv_quotient_of_eq h (quotient_group.mk x) = (quotient_group.mk x) :=
+lemma quotient_mul_equiv_of_eq_mk {M N : subgroup G} [M.normal] [N.normal] (h : M = N) (x : G) :
+  quotient_group.quotient_mul_equiv_of_eq h (quotient_group.mk x) = (quotient_group.mk x) :=
 rfl
 
 /-- Let `A', A, B', B` be subgroups of `G`. If `A' ≤ B'` and `A ≤ B`,
@@ -405,7 +402,7 @@ have φ_surjective : function.surjective φ := λ x, x.induction_on' $
     change h⁻¹ * (h * n) ∈ N,
     rwa [←mul_assoc, inv_mul_self, one_mul],
   end,
-(equiv_quotient_of_eq (by simp [comap_comap, ←comap_ker])).trans
+(quotient_mul_equiv_of_eq (by simp [comap_comap, ←comap_ker])).trans
   (quotient_ker_equiv_of_surjective φ φ_surjective)
 
 end snd_isomorphism_thm

src/ring_theory/valuation/valuation_subring.lean

@@ -619,7 +619,7 @@ the units of the residue field of `A`. -/
 def units_mod_principal_units_equiv_residue_field_units :
   (A.unit_group ⧸ (A.principal_unit_group.comap A.unit_group.subtype)) ≃*
   (local_ring.residue_field A)ˣ :=
-mul_equiv.trans (quotient_group.equiv_quotient_of_eq A.ker_unit_group_to_residue_field_units.symm)
+(quotient_group.quotient_mul_equiv_of_eq A.ker_unit_group_to_residue_field_units.symm).trans
   (quotient_group.quotient_ker_equiv_of_surjective _ A.surjective_unit_group_to_residue_field_units)
 
 @[simp]