G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ relindex (subgroupOf H L) (subgroupOf K L) * relindex K L = relindex H L
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ relindex H K * relindex K L = relindex H L
rw [← relindex_subgroupOf hKL]
no goals
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ relindex (subgroupOf H L) (subgroupOf K L) * relindex K L = relindex H L
exact relindex_mul_index fun x hx => hHK hx