apply generate_forget_adjunction
case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ pull f = Set.preimage ⇑f ∘ forget

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ forget ∘ pull f = Set.preimage ⇑f ∘ forget