intro S
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ∀ (s : Set (Subgroup G')), pull f (Inf s) = Inf (pull f '' s)
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
⊢ pull f (Inf S) = Inf (pull f '' S)