G : Type u_2
inst✝¹ : Group G
H✝ K✝ L : Subgroup G
H : Type u_1
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ Nat.card { x // x ∈ map f K } = Nat.card ↑(↑f '' ↑K)
G : Type u_2
inst✝¹ : Group G
H✝ K✝ L : Subgroup G
H : Type u_1
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ relindex (MonoidHom.ker f) K = Nat.card ↑(↑f '' ↑K)
rw [← MonoidHom.comap_bot, relindex_comap, relindex_bot_left]
no goals
G : Type u_2
inst✝¹ : Group G
H✝ K✝ L : Subgroup G
H : Type u_1
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ Nat.card { x // x ∈ map f K } = Nat.card ↑(↑f '' ↑K)
rfl