G✝ : Type ?u.97421
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Injective ↑f
⊢ Nat.card { x // x ∈ MonoidHom.range f } ∣ Nat.card H
G✝ : Type ?u.97421
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Injective ↑f
⊢ Nat.card G ∣ Nat.card H
rw [Nat.card_congr (MonoidHom.ofInjective hf).toEquiv]
no goals
G✝ : Type ?u.97421
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Injective ↑f
⊢ Nat.card { x // x ∈ MonoidHom.range f } ∣ Nat.card H
exact Dvd.intro f.range.index f.range.card_mul_index