G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_1
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), relindex (f i) ⊤ ≠ 0
⊢ relindex (⨅ (i : ι), f i) ⊤ ≠ 0
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_1
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), index (f i) ≠ 0
⊢ index (⨅ (i : ι), f i) ≠ 0
simp_rw [← relindex_top_right] at hf⊢
no goals
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_1
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), relindex (f i) ⊤ ≠ 0
⊢ relindex (⨅ (i : ι), f i) ⊤ ≠ 0
exact relindex_iInf_ne_zero hf