G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : MonoidHom.ker f ≤ H
⊢ index H ∣ index H * index (MonoidHom.range f)
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : MonoidHom.ker f ≤ H
⊢ index H ∣ index (map f H)
rw [index_map, sup_of_le_left hf]
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 : MonoidHom.ker f ≤ H
⊢ index H ∣ index H * index (MonoidHom.range f)
apply dvd_mul_right