A B : GroupCat
f : A ⟶ B
x : ↑B
⊢ ↑((τ.symm.trans (↑g x)).trans τ)
      (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) }) =
    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) }
A B : GroupCat
f : A ⟶ B
x : ↑B
⊢ ↑(↑h x)
      (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) }) =
    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) }
change ((τ).symm.trans (g x)).trans τ _ = _
no goals
A B : GroupCat
f : A ⟶ B
x : ↑B
⊢ ↑((τ.symm.trans (↑g x)).trans τ)
      (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) }) =
    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) }
simp [τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]