no goals
A B : GroupCat
f : A ⟶ B
x : ↑B
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ x *l ↑y ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
aesop_cat