ext H
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ forget ∘ pull f = Set.preimage ⇑f ∘ forget
case h.h.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
H : Subgroup G'
x✝ : G
⊢ x✝ ∈ (forget ∘ pull f) H ↔ x✝ ∈ (Set.preimage ⇑f ∘ forget) H