Theorem: Tutorial.Subgroups.SubgroupInf_carrier (GlimpseOfLean/Exercises/Topics/GaloisAdjunctions.lean)

State before:
G : Type
inst✝ : Group G
s : Set (Subgroup G)
⊢ (SubgroupInf s).carrier = ⋂₀ (Subgroup.carrier '' s)
Tactic:
simp [SubgroupInf]
State after:
no goals