[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N
[PROOFSTEP]
convert congr_arg LinearMap.range (underlyingIso_arrow (↾N.subtype : of R { x // x ∈ N } ⟶ M)) using 1
[GOAL]
case h.e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) =
    LinearMap.range ((underlyingIso (↾(Submodule.subtype N))).inv ≫ arrow (Subobject.mk (↾(Submodule.subtype N))))
[PROOFSTEP]
have :
  -- Porting note: added the `.toLinearEquiv.toLinearMap`(underlyingIso (↾N.subtype : of R _ ⟶ M)).inv =
    (underlyingIso (↾N.subtype : of R _ ⟶ M)).symm.toLinearEquiv.toLinearMap :=
  by
  apply LinearMap.ext
  intro x
  rfl
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (underlyingIso (↾(Submodule.subtype N))).inv = ↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm)
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ ∀ (x : ↑(of R { x // x ∈ N })),
    ↑(underlyingIso (↾(Submodule.subtype N))).inv x =
      ↑↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
x : ↑(of R { x // x ∈ N })
⊢ ↑(underlyingIso (↾(Submodule.subtype N))).inv x =
    ↑↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm) x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↾(Submodule.subtype N))).inv = ↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm)
⊢ (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) =
    LinearMap.range ((underlyingIso (↾(Submodule.subtype N))).inv ≫ arrow (Subobject.mk (↾(Submodule.subtype N))))
[PROOFSTEP]
rw [this, comp_def, LinearEquiv.range_comp]
[GOAL]
case h.e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = LinearMap.range (↾(Submodule.subtype N))
[PROOFSTEP]
exact (Submodule.range_subtype _).symm
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ S = (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S)
[PROOFSTEP]
fapply eq_mk_of_comm
[GOAL]
case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ underlying.obj S ≅ of R { x // x ∈ (fun S => LinearMap.range (arrow S)) S }
[PROOFSTEP]
apply LinearEquiv.toModuleIso'Left
[GOAL]
case i.e
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ↑(underlying.obj S) ≃ₗ[R] { x // x ∈ (fun S => LinearMap.range (arrow S)) S }
[PROOFSTEP]
apply LinearEquiv.ofBijective (LinearMap.codRestrict (LinearMap.range S.arrow) S.arrow _)
[GOAL]
case i.e
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Bijective ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S) ?m.95491)
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), ↑(arrow S) c ∈ LinearMap.range (arrow S)
[PROOFSTEP]
constructor
[GOAL]
case i.e.left
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Injective ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S) ?m.95491)
[PROOFSTEP]
simp [← LinearMap.ker_eq_bot, LinearMap.ker_codRestrict]
[GOAL]
case i.e.left
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ LinearMap.ker (arrow S) = ⊥
[PROOFSTEP]
rw [ker_eq_bot_of_mono]
[GOAL]
case i.e.right
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Surjective ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S) ?m.95491)
[PROOFSTEP]
rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, Submodule.comap_subtype_self]
[GOAL]
case i.e.right.hf
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), ↑(arrow S) c ∈ LinearMap.range (arrow S)
[PROOFSTEP]
exact LinearMap.mem_range_self _
[GOAL]
case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ (LinearEquiv.toModuleIso'Left
          (LinearEquiv.ofBijective
            (LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
              (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))
            (_ :
              Function.Injective
                  ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                      (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S))) ∧
                Function.Surjective
                  ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                      (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))))).hom ≫
      ↾(Submodule.subtype ((fun S => LinearMap.range (arrow S)) S)) =
    arrow S
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case w.h
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (x : ↑(underlying.obj S)),
    ↑((LinearEquiv.toModuleIso'Left
                (LinearEquiv.ofBijective
                  (LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                    (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))
                  (_ :
                    Function.Injective
                        ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                            (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S))) ∧
                      Function.Surjective
                        ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                            (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))))).hom ≫
            ↾(Submodule.subtype ((fun S => LinearMap.range (arrow S)) S)))
        x =
      ↑(arrow S) x
[PROOFSTEP]
intro x
[GOAL]
case w.h
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
x : ↑(underlying.obj S)
⊢ ↑((LinearEquiv.toModuleIso'Left
              (LinearEquiv.ofBijective
                (LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                  (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))
                (_ :
                  Function.Injective
                      ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                          (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S))) ∧
                    Function.Surjective
                      ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                          (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))))).hom ≫
          ↾(Submodule.subtype ((fun S => LinearMap.range (arrow S)) S)))
      x =
    ↑(arrow S) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
⊢ ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
            left_inv :=
              (_ :
                ∀ (N : Submodule R ↑M),
                  (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
            right_inv :=
              (_ :
                ∀ (S : Subobject M),
                  (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
        S ≤
      ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
            left_inv :=
              (_ :
                ∀ (N : Submodule R ↑M),
                  (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
            right_inv :=
              (_ :
                ∀ (S : Subobject M),
                  (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
        T ↔
    S ≤ T
[PROOFSTEP]
refine' ⟨fun h => _, fun h => mk_le_mk_of_comm (↟(Submodule.ofLe h)) rfl⟩
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      S ≤
    ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      T
⊢ S ≤ T
[PROOFSTEP]
convert LinearMap.range_comp_le_range (ofMkLEMk _ _ h) (↾T.subtype)
[GOAL]
case h.e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      S ≤
    ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      T
⊢ S =
    LinearMap.range
      (LinearMap.comp (↾(Submodule.subtype T)) (ofMkLEMk (↾(Submodule.subtype S)) (↾(Submodule.subtype T)) h))
[PROOFSTEP]
simpa only [← comp_def, ofMkLEMk_comp] using (Submodule.range_subtype _).symm
[GOAL]
case h.e'_4
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      S ≤
    ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      T
⊢ T = LinearMap.range (↾(Submodule.subtype T))
[PROOFSTEP]
exact (Submodule.range_subtype _).symm
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ ↑(arrow (kernelSubobject f)) (↑toKernelSubobject x) = ↑x
[PROOFSTEP]
suffices ((arrow ((kernelSubobject f))) ∘ (kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = x by convert this
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
this : (↑(arrow (kernelSubobject f)) ∘ ↑(kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = ↑x
⊢ ↑(arrow (kernelSubobject f)) (↑toKernelSubobject x) = ↑x
[PROOFSTEP]
convert this
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ (↑(arrow (kernelSubobject f)) ∘ ↑(kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = ↑x
[PROOFSTEP]
rw [Iso.trans_inv, ← coe_comp, Category.assoc]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ ↑((kernelIsoKer f).inv ≫ (kernelSubobjectIso f).inv ≫ arrow (kernelSubobject f)) x = ↑x
[PROOFSTEP]
simp only [Category.assoc, kernelSubobject_arrow', kernelIsoKer_inv_kernel_ι]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ ↑(Submodule.subtype (LinearMap.ker f)) x = ↑x
[PROOFSTEP]
aesop_cat
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
x y : ↑N
l : ↑L
w : x = y + ↑g (↑(factorThruImageSubobject f) l)
⊢ ↑(cokernel.π g) x = ↑(cokernel.π g) y
[PROOFSTEP]
subst w
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑(cokernel.π g) (y + ↑g (↑(factorThruImageSubobject f) l)) = ↑(cokernel.π g) y
[PROOFSTEP]
simp only [map_add, add_right_eq_self]
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑(cokernel.π g) (↑g (↑(factorThruImageSubobject f) l)) = 0
[PROOFSTEP]
change ((cokernel.π g) ∘ (g) ∘ (factorThruImageSubobject f)) l = 0
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ (↑(cokernel.π g) ∘ ↑g ∘ ↑(factorThruImageSubobject f)) l = 0
[PROOFSTEP]
rw [← coe_comp, ← coe_comp, Category.assoc]
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑(factorThruImageSubobject f ≫ g ≫ cokernel.π g) l = 0
[PROOFSTEP]
simp only [cokernel.condition, comp_zero]
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑0 l = 0
[PROOFSTEP]
rfl


[GOAL]
⊢ ConcreteCategory GroupCat
[PROOFSTEP]
dsimp only [GroupCat]
[GOAL]
⊢ ConcreteCategory (Bundled Group)
[PROOFSTEP]
infer_instance
[GOAL]
R S : GroupCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
[GOAL]
⊢ ConcreteCategory CommGroupCat
[PROOFSTEP]
dsimp only [CommGroupCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommGroup)
[PROOFSTEP]
infer_instance
[GOAL]
R S : CommGroupCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
[GOAL]
G : AddCommGroupCat
h k : ↑G
w : asHom h = asHom k
⊢ h = k
[PROOFSTEP]
convert congr_arg (fun k : AddCommGroupCat.of ℤ ⟶ G => (k : ℤ → G) (1 : ℤ)) w
[GOAL]
case h.e'_2
G : AddCommGroupCat
h k : ↑G
w : asHom h = asHom k
⊢ h = ↑(asHom h) 1
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
G : AddCommGroupCat
h k : ↑G
w : asHom h = asHom k
⊢ k = ↑(asHom k) 1
[PROOFSTEP]
simp
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ g₁ = g₂
[PROOFSTEP]
have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by aesop_cat
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ asHom g₁ ≫ f = asHom g₂ ≫ f
[PROOFSTEP]
aesop_cat
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂
[PROOFSTEP]
have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂
[PROOFSTEP]
apply asHom_injective t1
[GOAL]
α : Type u
⊢ (fun g => g.toEquiv) 1 = 1
[PROOFSTEP]
aesop
[GOAL]
α : Type u
⊢ ∀ (x y : ↑(GroupCat.of (Aut α))),
    OneHom.toFun { toFun := fun g => g.toEquiv, map_one' := (_ : (fun g => g.toEquiv) 1 = 1) } (x * y) =
      OneHom.toFun { toFun := fun g => g.toEquiv, map_one' := (_ : (fun g => g.toEquiv) 1 = 1) } x *
        OneHom.toFun { toFun := fun g => g.toEquiv, map_one' := (_ : (fun g => g.toEquiv) 1 = 1) } y
[PROOFSTEP]
aesop
[GOAL]
α : Type u
⊢ (fun g => Equiv.toIso g) 1 = 1
[PROOFSTEP]
aesop
[GOAL]
α : Type u
⊢ ∀ (x y : ↑(GroupCat.of (Equiv.Perm α))),
    OneHom.toFun { toFun := fun g => Equiv.toIso g, map_one' := (_ : (fun g => Equiv.toIso g) 1 = 1) } (x * y) =
      OneHom.toFun { toFun := fun g => Equiv.toIso g, map_one' := (_ : (fun g => Equiv.toIso g) 1 = 1) } x *
        OneHom.toFun { toFun := fun g => Equiv.toIso g, map_one' := (_ : (fun g => Equiv.toIso g) 1 = 1) } y
[PROOFSTEP]
aesop
[GOAL]
X Y : GroupCat
f : X ⟶ Y
x✝ : IsIso ((forget GroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget GroupCat).map f)
[GOAL]
X Y : GroupCat
f : X ⟶ Y
x✝ : IsIso ((forget GroupCat).map f)
i : (forget GroupCat).obj X ≅ (forget GroupCat).obj Y := asIso ((forget GroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f))
[GOAL]
X Y : GroupCat
f : X ⟶ Y
x✝ : IsIso ((forget GroupCat).map f)
i : (forget GroupCat).obj X ≅ (forget GroupCat).obj Y := asIso ((forget GroupCat).map f)
e : ↑X ≃* ↑Y :=
  { toEquiv := i.toEquiv,
    map_mul' :=
      (_ :
        ∀ (a b : ↑X),
          ↑(let_fun this := f;
                this)
              (a * b) =
            ↑(let_fun this := f;
                  this)
                a *
              ↑(let_fun this := f;
                  this)
                b) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toGroupCatIso
[GOAL]
X Y : CommGroupCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommGroupCat).map f)
[GOAL]
X Y : CommGroupCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGroupCat).map f)
i : (forget CommGroupCat).obj X ≅ (forget CommGroupCat).obj Y := asIso ((forget CommGroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f))
[GOAL]
X Y : CommGroupCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGroupCat).map f)
i : (forget CommGroupCat).obj X ≅ (forget CommGroupCat).obj Y := asIso ((forget CommGroupCat).map f)
e : ↑X ≃* ↑Y :=
  { toEquiv := i.toEquiv,
    map_mul' :=
      (_ :
        ∀ (a b : ↑X),
          ↑(let_fun this := f;
                this)
              (a * b) =
            ↑(let_fun this := f;
                  this)
                a *
              ↑(let_fun this := f;
                  this)
                b) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toCommGroupCatIso


[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