Theorem: Tutorial.Subgroups.generate_forget_adjunction (GlimpseOfLean/Solutions/Topics/GaloisAdjunctions.lean)

State before:
G : Type
inst✝ : Group G
⊢ adjunction generate forget
Tactic:
exact adjunction_of_Inf SubgroupInf_carrier
State after:
no goals