feat(group_theory/index): relindex_dvd_of_le_left (#9835)

If `H ≤ K`, then `K.relindex L ∣ H.relindex L`.

Caution: `relindex_dvd_of_le_right` is not true. `relindex_le_of_le_right` is true, but it is harder to prove, and harder to state (because you have to be careful about `relindex = 0`).

src/group_theory/index.lean

@@ -92,6 +92,27 @@ end
 
 variables (H K L)
 
+lemma inf_relindex_right : (H ⊓ K).relindex K = H.relindex K :=
+begin
+  rw [←subgroup_of_map_subtype, relindex, relindex, subgroup_of, comap_map_eq_self_of_injective],
+  exact subtype.coe_injective,
+end
+
+lemma inf_relindex_left : (H ⊓ K).relindex H = K.relindex H :=
+by rw [inf_comm, inf_relindex_right]
+
+variables {H K}
+
+lemma relindex_dvd_of_le_left (hHK : H ≤ K) :
+  K.relindex L ∣ H.relindex L :=
+begin
+  apply dvd_of_mul_left_eq ((H ⊓ L).relindex (K ⊓ L)),
+  rw [←inf_relindex_right H L, ←inf_relindex_right K L],
+  exact relindex_mul_relindex (inf_le_inf_right L hHK) inf_le_right,
+end
+
+variables (H K)
+
 @[simp, to_additive] lemma index_top : (⊤ : subgroup G).index = 1 :=
 cardinal.to_nat_eq_one_iff_unique.mpr ⟨quotient_group.subsingleton_quotient_top, ⟨1⟩⟩