no goals
A B : GroupCat
f : A ⟶ B
⊢ ↑τ.symm ∞ =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
rw [tau, Equiv.symm_swap, Equiv.swap_apply_right]