awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : (↑(F.obj j) : Type w)
rw :
  Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            ((toCocone F f).ι.app j) :
          (a : (↑(F.obj j) : Type w)) → (↑(toCocone F f).pt : Type w))
        x :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(toCocone F f).pt : Type w))
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (Y := (toCocone F f).pt) (c.ι.app j ≫ hc.desc (toCocone F f)) :
          (a : (↑(F.obj j) : Type w)) → (↑(toCocone F f).pt : Type w))
        x :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(toCocone F f).pt : Type w))

Tactic:
rw [hc.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            ((toCocone F f).ι.app j) :
          (a : (↑(F.obj j) : Type w)) → (↑(toCocone F f).pt : Type w))
        x :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → (↑(toCocone F f).pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(toCocone F f).pt : Type w))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
rw :
  (((AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) : Quot F →+ (↑(toCocone F f).pt : Type w)) :
        (a : Quot F) → A)
      x :
    A)
| ((f : (a : Quot F) → A) x : A)

Tactic:
rw [← Quot.desc_toCocone_desc F c f hc]

Premises used: AddCommGrpCat.Colimits.Quot.desc_toCocone_desc
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
conv_rhs :
  Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (Y := (toCocone F f).pt) (hc.desc (toCocone F f)) :
          (a : (↑c.pt : Type w)) → (↑(toCocone F f).pt : Type w))
        ((desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑(toCocone F f).pt : Type w))
    (((AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) : Quot F →+ (↑(toCocone F f).pt : Type w)) :
          (a : Quot F) → A)
        x :
      A)
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (Y := (toCocone F f).pt) (hc.desc (toCocone F f)) :
          (a : (↑c.pt : Type w)) → (↑(toCocone F f).pt : Type w))
        ((desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑(toCocone F f).pt : Type w))
    ((f : (a : Quot F) → A) x : A)

Tactic:
conv_rhs => rw [← Quot.desc_toCocone_desc F c f hc]

Premises used: AddCommGrpCat.Colimits.Quot.desc_toCocone_desc
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (Y := (toCocone F f).pt) (hc.desc (toCocone F f)) :
          (a : (↑c.pt : Type w)) → (↑(toCocone F f).pt : Type w))
        ((desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑(toCocone F f).pt : Type w))
    (((AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) : Quot F →+ (↑(toCocone F f).pt : Type w)) :
          (a : Quot F) → A)
        x :
      A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
hf :
  ∀ (x : (↑(F.obj j) : Type w)),
    Eq (α := (↑s.pt : Type w))
      ((Hom.hom
              (c.ι.app j ≫
                ofHom
                  (AddMonoidHom.comp (Quot.desc F s)
                    (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
            (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w))
          x :
        (↑s.pt : Type w))
      ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
⊢ c.ι.app j ≫
      ofHom
        (AddMonoidHom.comp (Quot.desc F s)
          (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h)))) =
    s.ι.app j

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
hf :
  Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Hom.hom (c.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w)) x)) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom
            (c.ι.app j ≫
              ofHom
                (AddMonoidHom.comp (Quot.desc F s)
                  (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
          (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
erw :
  ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
      ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
        ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x))) :
    (↑s.pt : Type w))
| ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
      ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
        ((Hom.hom (c.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w)) x)) :
    (↑s.pt : Type w))

Tactic:
erw [← Quot.ι_desc F c j x]

Premises used: AddCommGrpCat.Colimits.Quot.ι_desc
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
hf :
  Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x))) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
⊢ Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Hom.hom (c.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w)) x)) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))

Tactic:
conv_lhs => erw [← Quot.ι_desc F c j x]

Premises used: AddCommGrpCat.Colimits.Quot.ι_desc
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
hf :
  Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
⊢ Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x))) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))

Tactic:
rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]

Premises used: AddEquiv.symm_apply_apply, AddEquiv.ofBijective_apply
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑s.pt : Type w))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))

Tactic:
simp only [Quot.ι_desc, Functor.const_obj_obj]

Premises used: AddCommGrpCat.Colimits.Quot.ι_desc, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
hf :
  ∀ (x : (↑c.pt : Type w)),
    Eq (α := (↑s.pt : Type w)) ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
      ((Hom.hom
              (ofHom
                (AddMonoidHom.comp (Quot.desc F s)
                  (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
            (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
          x :
        (↑s.pt : Type w))
⊢ m =
    ofHom
      (AddMonoidHom.comp (Quot.desc F s)
        (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : (↑c.pt : Type w)
hf :
  ∀ (x : Quot F),
    Eq (α := (↑s.pt : Type w))
      ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
          ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
        (↑s.pt : Type w))
      ((Hom.hom
              (ofHom
                (AddMonoidHom.comp (Quot.desc F s)
                  (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
            (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
          ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
        (↑s.pt : Type w))
⊢ Eq (α := (↑s.pt : Type w)) ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
    ((Hom.hom
            (ofHom
              (AddMonoidHom.comp (Quot.desc F s)
                (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h))))) :
          (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))

Tactic:
obtain ⟨x, rfl⟩ := h.2 x

Premises used: And.right, rfl
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
hf :
  Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) x : (↑s.pt : Type w))
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w))
        ((AddEquiv.symm (AddEquiv.ofBijective (Quot.desc F c) h) : (a : (↑c.pt : Type w)) → Quot F)
          ((Quot.desc F c : (a : Quot F) → (↑c.pt : Type w)) x)) :
      (↑s.pt : Type w))

Tactic:
rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]

Premises used: AddEquiv.symm_apply_apply, AddEquiv.ofBijective_apply
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) = Quot.desc F s
rw :
  Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    (((Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) :
          (a : Quot F) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) x : (↑s.pt : Type w))

Tactic:
rw [← eq]
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) = Quot.desc F s
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    (((Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) :
          (a : Quot F) → (↑s.pt : Type w))
        x :
      (↑s.pt : Type w))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
hf : (Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) = Quot.desc F s
⊢ Eq (α := (↑s.pt : Type w))
    ((Hom.hom m : (a : (↑c.pt : Type w)) → (↑s.pt : Type w))
        ((AddEquiv.ofBijective (Quot.desc F c) h : (a : Quot F) → (↑c.pt : Type w)) x : (↑c.pt : Type w)) :
      (↑s.pt : Type w))
    ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) x : (↑s.pt : Type w))

Tactic:
suffices eq : m.hom.comp (AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s by
      rw [← eq]; rfl
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ ∀ (j : J) (x : (↑(F.obj j) : Type w)),
    Eq.{w + 1} (α := (↑s.pt : Type w))
      (((Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) :
            (a : Quot F) → (↑s.pt : Type w))
          ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
        (↑s.pt : Type w))
      ((Quot.desc F s : (a : Quot F) → (↑s.pt : Type w)) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
        (↑s.pt : Type w))

Tactic:
simp [← hm]
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Function.Bijective (α := Quot F) (β := (↑c.pt : Type w)) (⇑(Quot.desc F c) : (a : Quot F) → (↑c.pt : Type w))
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m).comp (↑(AddEquiv.ofBijective (Quot.desc F c) h) : Quot F →+ (↑c.pt : Type w)) = Quot.desc F s

Tactic:
exact Quot.addMonoidHom_ext F (by simp [← hm])

Premises used: AddCommGrpCat.Colimits.Quot.addMonoidHom_ext
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
inst_2 : Small.{w, max w u} (Quot F)
x x_1 : J
x_2 : x ⟶ x_1
hf :
  ∀ (x_3 : (↑(F.obj x) : Type w)),
    Eq (α :=
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
        Type w))
      ((Hom.hom
              (F.map x_2 ≫
                ofHom
                  (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                    (Quot.ι F x_1))) :
            (a : (↑(F.obj x) : Type w)) →
              (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
          x_3 :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
          Type w))
      ((Hom.hom
              (ofHom
                  (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                    (Quot.ι F x)) ≫
                CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_2) :
            (a : (↑(F.obj x) : Type w)) →
              (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
          x_3 :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
          Type w))
⊢ Eq (α :=
    F.obj x ⟶ Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1)
    (F.map x_2 ≫
        ofHom
          (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv)) (Quot.ι F x_1)) :
      F.obj x ⟶ Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1)
    (ofHom (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv)) (Quot.ι F x)) ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_2 :
      F.obj x ⟶ Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
inst_2 : Small.{w, max w u} (Quot F)
x x_1 : J
x_2 : x ⟶ x_1
x_3 : (↑(F.obj x) : Type w)
hf :
  Eq.{w + 1} (α := Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x_1 : (a : (↑(F.obj x_1) : Type w)) → Quot F)
            ((Hom.hom (F.map x_2) : (a : (↑(F.obj x) : Type w)) → (↑(F.obj x_1) : Type w)) x_3) :
          Quot F) :
      Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
      Shrink.{w, max u w} (Quot F))
⊢ Eq (α :=
    (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) : Type w))
    ((Hom.hom
            (F.map x_2 ≫
              ofHom
                (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                  (Quot.ι F x_1))) :
          (a : (↑(F.obj x) : Type w)) →
            (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
        x_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
        Type w))
    ((Hom.hom
            (ofHom
                (AddMonoidHom.comp (N := Quot F) (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))
                  (Quot.ι F x)) ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_2) :
          (a : (↑(F.obj x) : Type w)) →
            (↑(((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).obj x_1) : Type w))
        x_3 :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (Shrink.{w, max u w} (Quot F)))) x_1) :
        Type w))

Tactic:
dsimp