apply image_preimage_adjunction
case hXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (Set.image ↑f) ?uXY

case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

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 ∘ ?uZW = ?uXY ∘ ?uYW

case uXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Set G' → Set G

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

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 ∘ ?uZW = Set.preimage ↑f ∘ ?uYW

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G