[GOAL]
A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : { x // x ∈ ker f } →* A), comp f u = comp f v → u = v
⊢ ker f = ⊥
[PROOFSTEP]
simpa using _root_.congr_arg range (h f.ker.subtype 1 (by aesop_cat))
[GOAL]
A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : { x // x ∈ ker f } →* A), comp f u = comp f v → u = v
⊢ comp f (Subgroup.subtype (ker f)) = comp f 1
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
⊢ range f = ⊤
[PROOFSTEP]
specialize h 1 (QuotientGroup.mk' _) _
[GOAL]
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
⊢ comp 1 f = comp (QuotientGroup.mk' (range f)) f
[PROOFSTEP]
ext1 x
[GOAL]
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ ↑(comp 1 f) x = ↑(comp (QuotientGroup.mk' (range f)) f) x
[PROOFSTEP]
simp only [one_apply, coe_comp, coe_mk', Function.comp_apply]
[GOAL]
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ 1 = ↑(↑f x)
[PROOFSTEP]
rw [show (1 : B ⧸ f.range) = (1 : B) from QuotientGroup.mk_one _, QuotientGroup.eq, inv_one, one_mul]
[GOAL]
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ ↑f x ∈ range f
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' (range f)
⊢ range f = ⊤
[PROOFSTEP]
replace h : (QuotientGroup.mk' _).ker = (1 : B →* B ⧸ f.range).ker := by rw [h]
[GOAL]
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' (range f)
⊢ ker (QuotientGroup.mk' ?m.28184) = ker 1
[PROOFSTEP]
rw [h]
[GOAL]
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ker (QuotientGroup.mk' (range f)) = ker 1
⊢ range f = ⊤
[PROOFSTEP]
rwa [ker_one, QuotientGroup.ker_mk'] at h 
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ b *l ↑y ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
[PROOFSTEP]
rw [← y.2.choose_spec, leftCoset_assoc]
  -- Porting note: should we make `Bundled.α` reducible?
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ b *
        Exists.choose
          (_ : ↑y ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) *l
      (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier ∈
    Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
[PROOFSTEP]
let b' : B := y.2.choose
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
b' : ↑B :=
  Exists.choose (_ : ↑y ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ b *
        Exists.choose
          (_ : ↑y ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) *l
      (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier ∈
    Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
[PROOFSTEP]
use b * b'
[GOAL]
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
[PROOFSTEP]
change fromCoset _ = fromCoset _
[GOAL]
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)) }
[PROOFSTEP]
simp only [leftCoset_assoc]
[GOAL]
A B : GroupCat
f : A ⟶ B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ 1 • fromCoset y = fromCoset y
[PROOFSTEP]
change fromCoset _ = fromCoset _
[GOAL]
A B : GroupCat
f : A ⟶ B
x : X'
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ fromCoset
      { val := 1 *l ↑y,
        property :=
          (_ : 1 *l ↑y ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } =
    fromCoset y
[PROOFSTEP]
simp only [one_leftCoset, Subtype.ext_iff_val]
[GOAL]
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) }
[PROOFSTEP]
congr
[GOAL]
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
[PROOFSTEP]
let b : B.α := b
[GOAL]
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
[PROOFSTEP]
change b *l f.range = f.range
[GOAL]
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)
[PROOFSTEP]
nth_rw 2 [show (f.range : Set B.α) = 1 *l f.range from (one_leftCoset _).symm]
[GOAL]
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)
[PROOFSTEP]
rw [leftCoset_eq_iff, mul_one]
[GOAL]
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
[PROOFSTEP]
exact Subgroup.inv_mem _ hb
[GOAL]
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) }
[PROOFSTEP]
intro r
[GOAL]
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
[PROOFSTEP]
simp only [fromCoset.injEq, Subtype.mk.injEq] at r 
[GOAL]
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
[PROOFSTEP]
let b' : B.α := b
[GOAL]
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
[PROOFSTEP]
change b' *l f.range = f.range at r 
[GOAL]
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
[PROOFSTEP]
nth_rw 2 [show (f.range : Set B.α) = 1 *l f.range from (one_leftCoset _).symm] at r 
[GOAL]
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
[PROOFSTEP]
rw [leftCoset_eq_iff, mul_one] at r 
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ¬b ∈ MonoidHom.range f
b' : ↑B := b
r : b'⁻¹ ∈ MonoidHom.range f
⊢ False
[PROOFSTEP]
exact hb (inv_inv b ▸ Subgroup.inv_mem _ r)
[GOAL]
A B : GroupCat
f : A ⟶ B
⊢ ↑τ.symm
      (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) }) =
    ∞
[PROOFSTEP]
rw [tau, Equiv.symm_swap, Equiv.swap_apply_left]
[GOAL]
A B : GroupCat
f : A ⟶ B
⊢ ↑τ.symm ∞ =
    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) }
[PROOFSTEP]
rw [tau, Equiv.symm_swap, Equiv.swap_apply_right]
[GOAL]
A B : GroupCat
f : A ⟶ B
β : ↑B
x : X'
⊢ (fun x => β⁻¹ • x) ((fun x => β • x) x) = x
[PROOFSTEP]
dsimp only
[GOAL]
A B : GroupCat
f : A ⟶ B
β : ↑B
x : X'
⊢ β⁻¹ • β • x = x
[PROOFSTEP]
rw [← mul_smul, mul_left_inv, one_smul]
[GOAL]
A B : GroupCat
f : A ⟶ B
β : ↑B
x : X'
⊢ (fun x => β • x) ((fun x => β⁻¹ • x) x) = x
[PROOFSTEP]
dsimp only
[GOAL]
A B : GroupCat
f : A ⟶ B
β : ↑B
x : X'
⊢ β • β⁻¹ • x = x
[PROOFSTEP]
rw [← mul_smul, mul_right_inv, one_smul]
[GOAL]
A B : GroupCat
f : A ⟶ B
⊢ (fun β =>
        { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
          left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
          right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
      1 =
    1
[PROOFSTEP]
ext
[GOAL]
case H
A B : GroupCat
f : A ⟶ B
x✝ : X'
⊢ ↑((fun β =>
            { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
              left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
              right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
          1)
      x✝ =
    ↑1 x✝
[PROOFSTEP]
simp [one_smul]
[GOAL]
A B : GroupCat
f : A ⟶ B
b1 b2 : ↑B
⊢ OneHom.toFun
      {
        toFun := fun β =>
          { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
            left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
            right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) },
        map_one' :=
          (_ :
            (fun β =>
                  { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                    left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                    right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
                1 =
              1) }
      (b1 * b2) =
    OneHom.toFun
        {
          toFun := fun β =>
            { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
              left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
              right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) },
          map_one' :=
            (_ :
              (fun β =>
                    { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                      left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                      right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
                  1 =
                1) }
        b1 *
      OneHom.toFun
        {
          toFun := fun β =>
            { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
              left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
              right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) },
          map_one' :=
            (_ :
              (fun β =>
                    { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                      left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                      right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
                  1 =
                1) }
        b2
[PROOFSTEP]
ext
[GOAL]
case H
A B : GroupCat
f : A ⟶ B
b1 b2 : ↑B
x✝ : X'
⊢ ↑(OneHom.toFun
          {
            toFun := fun β =>
              { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) },
            map_one' :=
              (_ :
                (fun β =>
                      { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                        left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                        right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
                    1 =
                  1) }
          (b1 * b2))
      x✝ =
    ↑(OneHom.toFun
            {
              toFun := fun β =>
                { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                  left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                  right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) },
              map_one' :=
                (_ :
                  (fun β =>
                        { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                          left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                          right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
                      1 =
                    1) }
            b1 *
          OneHom.toFun
            {
              toFun := fun β =>
                { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                  left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                  right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) },
              map_one' :=
                (_ :
                  (fun β =>
                        { toFun := fun x => β • x, invFun := fun x => β⁻¹ • x,
                          left_inv := (_ : ∀ (x : X'), (fun x => β⁻¹ • x) ((fun x => β • x) x) = x),
                          right_inv := (_ : ∀ (x : X'), (fun x => β • x) ((fun x => β⁻¹ • x) x) = x) })
                      1 =
                    1) }
            b2)
      x✝
[PROOFSTEP]
simp [mul_smul]
[GOAL]
A B : GroupCat
f : A ⟶ B
⊢ (fun β => (τ.symm.trans (↑g β)).trans τ) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case H
A B : GroupCat
f : A ⟶ B
x✝ : X'
⊢ ↑((fun β => (τ.symm.trans (↑g β)).trans τ) 1) x✝ = ↑1 x✝
[PROOFSTEP]
simp
[GOAL]
A B : GroupCat
f : A ⟶ B
b1 b2 : ↑B
⊢ OneHom.toFun
      { toFun := fun β => (τ.symm.trans (↑g β)).trans τ,
        map_one' := (_ : (fun β => (τ.symm.trans (↑g β)).trans τ) 1 = 1) }
      (b1 * b2) =
    OneHom.toFun
        { toFun := fun β => (τ.symm.trans (↑g β)).trans τ,
          map_one' := (_ : (fun β => (τ.symm.trans (↑g β)).trans τ) 1 = 1) }
        b1 *
      OneHom.toFun
        { toFun := fun β => (τ.symm.trans (↑g β)).trans τ,
          map_one' := (_ : (fun β => (τ.symm.trans (↑g β)).trans τ) 1 = 1) }
        b2
[PROOFSTEP]
ext
[GOAL]
case H
A B : GroupCat
f : A ⟶ B
b1 b2 : ↑B
x✝ : X'
⊢ ↑(OneHom.toFun
          { toFun := fun β => (τ.symm.trans (↑g β)).trans τ,
            map_one' := (_ : (fun β => (τ.symm.trans (↑g β)).trans τ) 1 = 1) }
          (b1 * b2))
      x✝ =
    ↑(OneHom.toFun
            { toFun := fun β => (τ.symm.trans (↑g β)).trans τ,
              map_one' := (_ : (fun β => (τ.symm.trans (↑g β)).trans τ) 1 = 1) }
            b1 *
          OneHom.toFun
            { toFun := fun β => (τ.symm.trans (↑g β)).trans τ,
              map_one' := (_ : (fun β => (τ.symm.trans (↑g β)).trans τ) 1 = 1) }
            b2)
      x✝
[PROOFSTEP]
simp
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
y : ↑(Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
⊢ x *l ↑y ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
[PROOFSTEP]
aesop_cat
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑(↑h x) ∞ = ∞
[PROOFSTEP]
change ((τ).symm.trans (g x)).trans τ _ = _
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑((τ.symm.trans (↑g x)).trans τ) ∞ = ∞
[PROOFSTEP]
simp only [MonoidHom.coe_mk, Equiv.toFun_as_coe, Equiv.coe_trans, Function.comp_apply]
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
⊢ ↑τ (↑(↑g x) (↑τ.symm ∞)) = ∞
[PROOFSTEP]
rw [τ_symm_apply_infinity, g_apply_fromCoset]
[GOAL]
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)) }) =
    ∞
[PROOFSTEP]
simpa only using τ_apply_fromCoset' f x hx
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
⊢ ↑(↑h x)
      (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) }) =
    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) }
[PROOFSTEP]
change ((τ).symm.trans (g x)).trans τ _ = _
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
⊢ ↑((τ.symm.trans (↑g x)).trans τ)
      (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) }) =
    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) }
[PROOFSTEP]
simp [τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
⊢ ↑(↑h x)
      (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 := x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
[PROOFSTEP]
change ((τ).symm.trans (g x)).trans τ _ = _
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
⊢ ↑((τ.symm.trans (↑g x)).trans τ)
      (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 := x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
[PROOFSTEP]
simp only [tau, MonoidHom.coe_mk, Equiv.toFun_as_coe, Equiv.coe_trans, Function.comp_apply]
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
⊢ ↑(Equiv.swap
          (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) })
          ∞)
      (↑(↑g x)
        (↑(Equiv.swap
                (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) })
                ∞).symm
          (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 := x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
[PROOFSTEP]
rw [Equiv.symm_swap,
  @Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) ∞
    (fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
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) } ≠
    ∞
[PROOFSTEP]
simp
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
⊢ ↑(Equiv.swap
          (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) })
          ∞)
      (↑(↑g x)
        (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 := x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
[PROOFSTEP]
simp only [g_apply_fromCoset, leftCoset_assoc]
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
⊢ ↑(Equiv.swap
          (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) })
          ∞)
      (fromCoset
        { val := x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              (fun x => x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
                (x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }) =
    fromCoset
      { val := x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
[PROOFSTEP]
refine' Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb _) (by simp)
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
⊢ fromCoset
      { val := x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            (fun x => x ∈ Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier))
              (x * b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) } ≠
    ∞
[PROOFSTEP]
simp
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r : x * b ∈ MonoidHom.range f
⊢ b ∈ MonoidHom.range f
[PROOFSTEP]
convert Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r
[GOAL]
case h.e'_4
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : x ∈ MonoidHom.range f
b : ↑B
hb : ¬b ∈ MonoidHom.range f
r : x * b ∈ MonoidHom.range f
⊢ b = x⁻¹ * (x * b)
[PROOFSTEP]
rw [← mul_assoc, mul_left_inv, one_mul]
[GOAL]
A B : GroupCat
f : A ⟶ B
⊢ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = {x | ↑h x = ↑g x}
[PROOFSTEP]
refine' Set.ext fun b => ⟨_, fun hb : h b = g b => by_contradiction fun r => _⟩
[GOAL]
case refine'_1
A B : GroupCat
f : A ⟶ B
b : ↑B
⊢ b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier → b ∈ {x | ↑h x = ↑g x}
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case refine'_1.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ {x | ↑h x = ↑g x}
[PROOFSTEP]
change h (f a) = g (f a)
[GOAL]
case refine'_1.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑h (↑f a) = ↑g (↑f a)
[PROOFSTEP]
ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
[GOAL]
case refine'_1.intro.H.fromCoset.mk.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    ↑(↑g (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) })
[PROOFSTEP]
rw [g_apply_fromCoset]
[GOAL]
case refine'_1.intro.H.fromCoset.mk.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
[PROOFSTEP]
by_cases m : y ∈ f.range
[GOAL]
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
[PROOFSTEP]
rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
[GOAL]
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.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) } =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
[PROOFSTEP]
change fromCoset _ = fromCoset ⟨f a *l (y *l _), _⟩
[GOAL]
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.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) } =
    fromCoset
      { val := ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier),
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
[PROOFSTEP]
simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m)]
[GOAL]
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ fromCoset
      { val := ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y_1,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      { val := ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier),
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
[PROOFSTEP]
congr
[GOAL]
case pos.e_a.e_val
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier =
    ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
[PROOFSTEP]
rw [leftCoset_assoc _ (f a) y]
[GOAL]
case neg
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : ¬y ∈ MonoidHom.range f
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
[PROOFSTEP]
rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
[GOAL]
case neg
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : ¬y ∈ MonoidHom.range f
⊢ fromCoset
      { val := ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y_1,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
[PROOFSTEP]
simp only [leftCoset_assoc]
[GOAL]
case refine'_1.intro.H.infinity
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑(↑h (↑f a)) ∞ = ↑(↑g (↑f a)) ∞
[PROOFSTEP]
rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
[GOAL]
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ False
[PROOFSTEP]
have eq1 :
  (h b) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) = fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ :=
  by
  change ((τ).symm.trans (g b)).trans τ _ = _
  dsimp [tau]
  simp [g_apply_infinity f]
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑(↑h b)
      (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) }) =
    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) }
[PROOFSTEP]
change ((τ).symm.trans (g b)).trans τ _ = _
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑((τ.symm.trans (↑g b)).trans τ)
      (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) }) =
    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) }
[PROOFSTEP]
dsimp [tau]
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑(Equiv.swap
          (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) })
          ∞)
      (↑(↑g b)
        (↑(Equiv.swap
              (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) })
              ∞)
          (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) }))) =
    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) }
[PROOFSTEP]
simp [g_apply_infinity f]
[GOAL]
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (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) }) =
    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
[PROOFSTEP]
have eq2 : (g b) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) = fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩ := rfl
[GOAL]
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (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) }) =
    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) }
eq2 :
  ↑(↑g b)
      (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) }) =
    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) }
⊢ False
[PROOFSTEP]
exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, FunLike.congr_fun hb])
[GOAL]
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (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) }) =
    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) }
eq2 :
  ↑(↑g b)
      (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) }) =
    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) } =
    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) }
[PROOFSTEP]
rw [← eq1, ← eq2, FunLike.congr_fun hb]
[GOAL]
A B : GroupCat
f : A ⟶ B
⊢ (f ≫
      let_fun this := g;
      this) =
    f ≫
      let_fun this := h;
      this
[PROOFSTEP]
ext a
[GOAL]
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑(f ≫
          let_fun this := g;
          this)
      a =
    ↑(f ≫
          let_fun this := h;
          this)
      a
[PROOFSTEP]
change g (f a) = h (f a)
[GOAL]
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑g (↑f a) = ↑h (↑f a)
[PROOFSTEP]
have : f a ∈ {b | h b = g b} := by
  rw [← agree]
  use a
[GOAL]
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ {b | ↑h b = ↑g b}
[PROOFSTEP]
rw [← agree]
[GOAL]
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
use a
[GOAL]
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
this : ↑f a ∈ {b | ↑h b = ↑g b}
⊢ ↑g (↑f a) = ↑h (↑f a)
[PROOFSTEP]
rw [this]
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
⊢ g ≠ h
[PROOFSTEP]
intro r
[GOAL]
A B : GroupCat
f : A ⟶ B
x : ↑B
hx : ¬x ∈ MonoidHom.range f
r : g = h
⊢ False
[PROOFSTEP]
replace r := FunLike.congr_fun (FunLike.congr_fun r x) (fromCoset ⟨f.range, ⟨1, one_leftCoset _⟩⟩)
[GOAL]
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
[PROOFSTEP]
change _ = ((τ).symm.trans (g x)).trans τ _ at r 
[GOAL]
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
[PROOFSTEP]
rw [g_apply_fromCoset, MonoidHom.coe_mk] at r 
[GOAL]
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
[PROOFSTEP]
simp only [MonoidHom.coe_range, Subtype.coe_mk, Equiv.symm_swap, Equiv.toFun_as_coe, Equiv.coe_trans,
  Function.comp_apply] at r 
[GOAL]
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
[PROOFSTEP]
erw [Equiv.swap_apply_left, g_apply_infinity, Equiv.swap_apply_right] at r 
[GOAL]
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
[PROOFSTEP]
exact fromCoset_ne_of_nin_range _ hx r
[GOAL]
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
⊢ Function.Surjective ↑f
[PROOFSTEP]
by_contra r
[GOAL]
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ¬Function.Surjective ↑f
⊢ False
[PROOFSTEP]
dsimp [Function.Surjective] at r 
[GOAL]
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ¬∀ (b : ↑B), ∃ a, ↑f a = b
⊢ False
[PROOFSTEP]
push_neg at r 
[GOAL]
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ∃ b, ∀ (a : ↑A), ↑f a ≠ b
⊢ False
[PROOFSTEP]
rcases r with ⟨b, hb⟩
[GOAL]
case intro
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
b : ↑B
hb : ∀ (a : ↑A), ↑f a ≠ b
⊢ False
[PROOFSTEP]
exact SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc) ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f))
[GOAL]
A B : AddGroupCat
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f) :=
  by
  refine' ⟨_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
  intro e'
  apply groupAddGroupEquivalence.inverse.map_epi
[GOAL]
A B : AddGroupCat
f : A ⟶ B
⊢ Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
[PROOFSTEP]
refine' ⟨_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
[GOAL]
A B : AddGroupCat
f : A ⟶ B
⊢ Epi f → Epi (groupAddGroupEquivalence.inverse.map f)
[PROOFSTEP]
intro e'
[GOAL]
A B : AddGroupCat
f : A ⟶ B
e' : Epi f
⊢ Epi (groupAddGroupEquivalence.inverse.map f)
[PROOFSTEP]
apply groupAddGroupEquivalence.inverse.map_epi
[GOAL]
A B : AddGroupCat
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
rwa [GroupCat.epi_iff_surjective] at i1 
[GOAL]
A B : GroupCat
f✝ : A ⟶ B
X✝ Y✝ : GroupCat
f : X✝ ⟶ Y✝
e : Mono f
⊢ Mono ((forget GroupCat).map f)
[PROOFSTEP]
rwa [mono_iff_injective, ← CategoryTheory.mono_iff_injective] at e 
[GOAL]
A B : GroupCat
f✝ : A ⟶ B
X✝ Y✝ : GroupCat
f : X✝ ⟶ Y✝
e : Epi f
⊢ Epi ((forget GroupCat).map f)
[PROOFSTEP]
rwa [epi_iff_surjective, ← CategoryTheory.epi_iff_surjective] at e 
[GOAL]
A B : CommGroupCat
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [epi_iff_range_eq_top, MonoidHom.range_top_iff_surjective]
[GOAL]
A B : CommGroupCat
f✝ : A ⟶ B
X✝ Y✝ : CommGroupCat
f : X✝ ⟶ Y✝
e : Mono f
⊢ Mono ((forget CommGroupCat).map f)
[PROOFSTEP]
rwa [mono_iff_injective, ← CategoryTheory.mono_iff_injective] at e 
[GOAL]
A B : CommGroupCat
f✝ : A ⟶ B
X✝ Y✝ : CommGroupCat
f : X✝ ⟶ Y✝
e : Epi f
⊢ Epi ((forget CommGroupCat).map f)
[PROOFSTEP]
rwa [epi_iff_surjective, ← CategoryTheory.epi_iff_surjective] at e 
