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

State before:
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ push f ∘ generate = generate ∘ Set.image ⇑f
Tactic:
sorry
State after:
no goals