rw [SubgroupInf_carrier]
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (SubgroupInf s).carrier
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (⋂₀ (Subgroup.carrier '' s))