A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑((τ.symm.trans (↑g x)).trans τ) ∞ = ∞
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑(↑h x) ∞ = ∞
change ((τ).symm.trans (g x)).trans τ _ = _
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑τ (↑(↑g x) (↑τ.symm ∞)) = ∞
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑((τ.symm.trans (↑g x)).trans τ) ∞ = ∞
simp only [MonoidHom.coe_mk, Equiv.toFun_as_coe, Equiv.coe_trans, Function.comp_apply]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑τ
      (fromCoset
        {
          val :=
            x *l
              ↑{ 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) },
          property :=
            (_ :
              x *l
                  ↑{ 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) } ∈
                Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }) =
    ∞
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑τ (↑(↑g x) (↑τ.symm ∞)) = ∞
rw [τ_symm_apply_infinity, g_apply_fromCoset]
no goals
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑τ
      (fromCoset
        {
          val :=
            x *l
              ↑{ 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) },
          property :=
            (_ :
              x *l
                  ↑{ 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) } ∈
                Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }) =
    ∞
simpa only using τ_apply_fromCoset' f x hx