ext x
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.carrier.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
x : G
⊢ x ∈ (pull f (Inf S)).carrier ↔ x ∈ (Inf (pull f '' S)).carrier