feat(group_theory/coset): Embeddings of quotients (#10901)

If `K ≤ L`, then there is an embedding `K ⧸ (H.subgroup_of K) ↪ L ⧸ (H.subgroup_of L)`. Golfed from #9545.

src/group_theory/coset.lean

@@ -409,6 +409,12 @@ noncomputable def quotient_equiv_prod_of_le (h_le : s ≤ t) :
   α ⧸ s ≃ (α ⧸ t) × (t ⧸ s.subgroup_of t) :=
 quotient_equiv_prod_of_le' h_le quotient.out' quotient.out_eq'
 
+/-- If `K ≤ L`, then there is an embedding `K ⧸ (H.subgroup_of K) ↪ L ⧸ (H.subgroup_of L)`. -/
+def quotient_subgroup_of_embedding_of_le (H : subgroup α) {K L : subgroup α} (h : K ≤ L) :
+  K ⧸ (H.subgroup_of K) ↪ L ⧸ (H.subgroup_of L) :=
+{ to_fun := quotient.map' (set.inclusion h) (λ a b, id),
+  inj' := by refine quotient.ind₂' (λ a b, _); exact quotient.eq'.mpr ∘ quotient.eq'.mp }
+
 @[to_additive] lemma card_eq_card_quotient_mul_card_subgroup
   [fintype α] (s : subgroup α) [fintype s] [decidable_pred (λ a, a ∈ s)] :
   fintype.card α = fintype.card (α ⧸ s) * fintype.card s :=