A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r : g = h
⊢ False
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
⊢ g ≠ h
intro r
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  ↑(↑g x)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) }) =
    ↑(↑h x)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) })
⊢ False
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r : g = h
⊢ False
replace r :=
  FunLike.congr_fun (FunLike.congr_fun r x) (fromCoset ⟨f.range, ⟨1, one_leftCoset _⟩⟩)
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  ↑(↑g x)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) }) =
    ↑((τ.symm.trans (↑g x)).trans τ)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) })
⊢ False
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  ↑(↑g x)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) }) =
    ↑(↑h x)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) })
⊢ False
change _ = ((τ).symm.trans (g x)).trans τ _ at r
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  fromCoset
      {
        val :=
          x *l
            ↑{ val := ↑(MonoidHom.range f),
                property :=
                  (_ :
                    ∃ y,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                        ↑(MonoidHom.range f)) },
        property :=
          (_ :
            x *l
                ↑{ val := ↑(MonoidHom.range f),
                    property :=
                      (_ :
                        ∃ y,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                            ↑(MonoidHom.range f)) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } =
    ↑((τ.symm.trans (↑↑g x)).trans τ)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) })
⊢ False
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  ↑(↑g x)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) }) =
    ↑((τ.symm.trans (↑g x)).trans τ)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) })
⊢ False
rw [g_apply_fromCoset, MonoidHom.coe_mk] at r
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  fromCoset
      { val := x *l Set.range ↑f,
        property :=
          (_ :
            (fun x => x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
              (x *l Set.range ↑f)) } =
    ↑τ
      (↑(↑↑g x)
        (↑τ.symm
          (fromCoset
            { val := Set.range ↑f,
              property :=
                (_ :
                  (fun x =>
                      x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
                    (Set.range ↑f)) })))
⊢ False
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  fromCoset
      {
        val :=
          x *l
            ↑{ val := ↑(MonoidHom.range f),
                property :=
                  (_ :
                    ∃ y,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                        ↑(MonoidHom.range f)) },
        property :=
          (_ :
            x *l
                ↑{ val := ↑(MonoidHom.range f),
                    property :=
                      (_ :
                        ∃ y,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                            ↑(MonoidHom.range f)) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } =
    ↑((τ.symm.trans (↑↑g x)).trans τ)
      (fromCoset
        { val := ↑(MonoidHom.range f),
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  ↑(MonoidHom.range f)) })
⊢ False
simp only [MonoidHom.coe_range, Subtype.coe_mk, Equiv.symm_swap, Equiv.toFun_as_coe,
  Equiv.coe_trans, Function.comp_apply] at r
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  fromCoset
      { val := x *l Set.range ↑f,
        property :=
          (_ :
            (fun x => x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
              (x *l Set.range ↑f)) } =
    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) }
⊢ False
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  fromCoset
      { val := x *l Set.range ↑f,
        property :=
          (_ :
            (fun x => x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
              (x *l Set.range ↑f)) } =
    ↑τ
      (↑(↑↑g x)
        (↑τ.symm
          (fromCoset
            { val := Set.range ↑f,
              property :=
                (_ :
                  (fun x =>
                      x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
                    (Set.range ↑f)) })))
⊢ False
erw [Equiv.swap_apply_left, g_apply_infinity, Equiv.swap_apply_right] at r
no goals
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r :
  fromCoset
      { val := x *l Set.range ↑f,
        property :=
          (_ :
            (fun x => x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
              (x *l Set.range ↑f)) } =
    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) }
⊢ False
exact fromCoset_ne_of_nin_range _ hx r