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_left]