G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ index (H ⊔ MonoidHom.ker f) ∣ index H
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ index (map f H) ∣ index H
rw [index_map, f.range_top_of_surjective hf, index_top, mul_one]
no goals
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ index (H ⊔ MonoidHom.ker f) ∣ index H
exact index_dvd_of_le le_sup_left