no goals
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_1
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ index (⨅ (i : ι), f i) ≤ ∏ i : ι, index (f i)
simp_rw [← relindex_top_right, relindex_iInf_le]