case e_a.e_val
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : b ∈ MonoidHom.range f
⊢ b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
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) }
congr
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b✝ *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : b ∈ MonoidHom.range f
⊢ b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
let b : B.α := b
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b *l ↑(MonoidHom.range f) = ↑(MonoidHom.range f)
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b✝ *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
change b *l f.range = f.range
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b *l ↑(MonoidHom.range f) = 1 *l ↑(MonoidHom.range f)
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b *l ↑(MonoidHom.range f) = ↑(MonoidHom.range f)
nth_rw 2 [show (f.range : Set B.α) = 1 *l f.range from (one_leftCoset _).symm]
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b⁻¹ ∈ MonoidHom.range f
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b *l ↑(MonoidHom.range f) = 1 *l ↑(MonoidHom.range f)
rw [leftCoset_eq_iff, mul_one]
no goals
case e_a.e_val
A B : GroupCat
f : A ⟶ B
b✝ : ↑B
hb : b✝ ∈ MonoidHom.range f
b : ↑B := b✝
⊢ b⁻¹ ∈ MonoidHom.range f
exact Subgroup.inv_mem _ hb