no goals
G : Type u_2
inst✝¹ : Group G
H K✝ L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
K : Subgroup G'
⊢ relindex (comap f H) K = relindex H (map f K)
rw [relindex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.subtype_range]