no goals
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G →* G'
⊢ index (map f H) = index (H ⊔ MonoidHom.ker f) * index (MonoidHom.range f)
rw [← comap_map_eq, index_comap, relindex_mul_index (H.map_le_range f)]