A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r :
  fromCoset
      { val := b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                b *l (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) }
⊢ False
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
⊢ fromCoset
      { val := b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                b *l (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) }
intro r
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r : b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ False
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r :
  fromCoset
      { val := b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                b *l (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) }
⊢ False
simp only [fromCoset.injEq, Subtype.mk.injEq] at r
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r : b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
b' : ↑B := b
⊢ False
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r : b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ False
let b' : B.α := b
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
b' : ↑B := b
r : b' *l ↑(MonoidHom.range f) = ↑(MonoidHom.range f)
⊢ False
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r : b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
b' : ↑B := b
⊢ False
change b' *l f.range = f.range at r
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
b' : ↑B := b
r : b' *l ↑(MonoidHom.range f) = 1 *l ↑(MonoidHom.range f)
⊢ False
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
b' : ↑B := b
r : b' *l ↑(MonoidHom.range f) = ↑(MonoidHom.range f)
⊢ False
nth_rw 2 [show (f.range : Set B.α) = 1 *l f.range from (one_leftCoset _).symm] at r
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
b' : ↑B := b
r : b'⁻¹ ∈ MonoidHom.range f
⊢ False
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
b' : ↑B := b
r : b' *l ↑(MonoidHom.range f) = 1 *l ↑(MonoidHom.range f)
⊢ False
rw [leftCoset_eq_iff, mul_one] at r
no goals
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
b' : ↑B := b
r : b'⁻¹ ∈ MonoidHom.range f
⊢ False
exact hb (inv_inv b ▸ Subgroup.inv_mem _ r)