A B : GroupCat
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ fromCoset
      { val := b * b' *l ↑y,
        property :=
          (_ :
            b * b' *l ↑y ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } =
    fromCoset
      {
        val :=
          b *l
            ↑{ val := b' *l ↑y,
                property :=
                  (_ :
                    b' *l ↑y ∈
                      Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) },
        property :=
          (_ :
            b *l
                ↑{ val := b' *l ↑y,
                    property :=
                      (_ :
                        b' *l ↑y ∈
                          Set.range
                            (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
A B : GroupCat
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ (b * b') • fromCoset y = b • b' • fromCoset y
change fromCoset _ = fromCoset _
no goals
A B : GroupCat
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ fromCoset
      { val := b * b' *l ↑y,
        property :=
          (_ :
            b * b' *l ↑y ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } =
    fromCoset
      {
        val :=
          b *l
            ↑{ val := b' *l ↑y,
                property :=
                  (_ :
                    b' *l ↑y ∈
                      Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) },
        property :=
          (_ :
            b *l
                ↑{ val := b' *l ↑y,
                    property :=
                      (_ :
                        b' *l ↑y ∈
                          Set.range
                            (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
simp only [leftCoset_assoc]