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
inst_1 : DecidableEq J
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type w)
simp :
  HSub.hSub (α := Π₀ (j : J), (↑(F.obj j) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
          x))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j x) ∈
    Relations F
⊢ HSub.hSub (α := Π₀ (j : J), (↑(F.obj j) : Type w)) (β := Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j' :
              (↑(F.obj j') : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j') : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            x) :
        Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j :
              (↑(F.obj j) : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j) : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          x :
        Π₀ (j : J), (↑(F.obj j) : Type w)) ∈
    Relations F

Tactic:
simp only [DFinsupp.singleAddHom_apply]

Premises used: DFinsupp.singleAddHom_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
inst_1 : DecidableEq J
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type w)
⊢ HSub.hSub (α := Π₀ (j : J), (↑(F.obj j) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
          x))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j x) ∈
    Relations F

Tactic:
AddSubgroup.subset_closure ⟨j, j', f, x, rfl⟩

Premises used: Set.Mem, Exists.intro, rfl, AddSubgroup.subset_closure
-- 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
inst_1 : DecidableEq J
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type w)
⊢ HSub.hSub (α := Π₀ (j : J), (↑(F.obj j) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
          x))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j x) ∈
    Relations F

Tactic:
exact AddSubgroup.subset_closure ⟨j, j', f, x, 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
rw :
  {x : Π₀ (j : J), (↑(F.obj j) : Type w) |
      ∃ (j : J) (j' : J) (u : j ⟶ j') (a : (↑(F.obj j) : Type w)),
        x =
          HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
            (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
              ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    carrier) (F.map u) :
                  (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
                a))
            (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j a)} ⊆
    (↑(AddMonoidHom.ker (M := Quot (F ⋙ uliftFunctor))
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (j : J) ↦
            AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)))) :
      Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
⊢ Relations F ≤
    AddMonoidHom.ker (M := Quot (F ⋙ uliftFunctor))
      (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (j : J) ↦
        AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)))

Tactic:
rw [AddSubgroup.closure_le]

Premises used: AddSubgroup.closure_le
-- 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 : Π₀ (j : J), (↑(F.obj j) : Type w)
hx :
  Membership.mem (γ := Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
    {x : Π₀ (j : J), (↑(F.obj j) : Type w) |
      ∃ (j : J) (j' : J) (u : j ⟶ j') (a : (↑(F.obj j) : Type w)),
        x =
          HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
            (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
              ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    carrier) (F.map u) :
                  (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
                a))
            (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j a)}
    a
obtain :
  ∀ (j j' : J) (u : j ⟶ j') (a : (↑(F.obj j) : Type w)),
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
        (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map u) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            a))
        (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j a) ∈
      (↑(AddMonoidHom.ker (M := Quot (F ⋙ uliftFunctor))
            (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (j : J) ↦
              AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j)
                (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)))) :
        Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
⊢ a ∈
    (↑(AddMonoidHom.ker (M := Quot (F ⋙ uliftFunctor))
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (j : J) ↦
            AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)))) :
      Set (Π₀ (j : J), (↑(F.obj j) : Type w)))

Tactic:
obtain ⟨j, j', u, a, rfl⟩ := hx

Premises used: 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
j j' : J
u : j ⟶ j'
a : (↑(F.obj j) : Type w)
rw :
  HSub.hSub (α := Quot (F ⋙ uliftFunctor)) (β := Quot (F ⋙ uliftFunctor))
      ((AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j') (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) :
            (a : (↑(F.obj j') : Type w)) → Quot (F ⋙ uliftFunctor))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map u) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            a) :
        Quot (F ⋙ uliftFunctor))
      ((AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) :
            (a : (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
          a :
        Quot (F ⋙ uliftFunctor)) =
    0
⊢ HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map u) :
            (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
          a))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j a) ∈
    (↑(AddMonoidHom.ker (M := Quot (F ⋙ uliftFunctor))
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (j : J) ↦
            AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)))) :
      Set (Π₀ (j : J), (↑(F.obj j) : Type w)))

Tactic:
rw [SetLike.mem_coe, AddMonoidHom.mem_ker, map_sub, DFinsupp.sumAddHom_single,
    DFinsupp.sumAddHom_single]

Premises used: map_sub, DFinsupp.sumAddHom_single, SetLike.mem_coe, AddMonoidHom.mem_ker
-- 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
j j' : J
u : j ⟶ j'
a : (↑(F.obj j) : Type w)
change :
  HSub.hSub (α := Quot (F ⋙ uliftFunctor)) (β := Quot (F ⋙ uliftFunctor))
      ((Quot.ι (F ⋙ uliftFunctor) j' : (a : (↑((F ⋙ uliftFunctor).obj j') : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max w u')) →+ (↑x2 : Type (max w u'))) (CC := carrier) ((F ⋙ uliftFunctor).map u) :
              (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → (↑((F ⋙ uliftFunctor).obj j') : Type (max w u')))
            ((AddEquiv.symm AddEquiv.ulift : (a : (↑(F.obj j) : Type w)) → ULift.{u', w} (↑(F.obj j) : Type w)) a)) :
        Quot (F ⋙ uliftFunctor))
      ((AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) :
            (a : (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
          a :
        Quot (F ⋙ uliftFunctor)) =
    0
⊢ HSub.hSub (α := Quot (F ⋙ uliftFunctor)) (β := Quot (F ⋙ uliftFunctor))
      ((AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j') (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) :
            (a : (↑(F.obj j') : Type w)) → Quot (F ⋙ uliftFunctor))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map u) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            a) :
        Quot (F ⋙ uliftFunctor))
      ((AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) :
            (a : (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
          a :
        Quot (F ⋙ uliftFunctor)) =
    0

Tactic:
change Quot.ι (F ⋙ uliftFunctor) j' ((F ⋙ uliftFunctor).map u (AddEquiv.ulift.symm a)) - _ = _

Premises used: AddCommGrpCat.uliftFunctor, CategoryTheory.ConcreteCategory.hom, AddEquiv.ulift, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, AddCommGrpCat.Colimits.Quot.ι, DFunLike.coe, AddEquiv.symm
-- 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
j j' : J
u : j ⟶ j'
a : (↑(F.obj j) : Type w)
rw :
  HSub.hSub (α := Quot (F ⋙ uliftFunctor)) (β := Quot (F ⋙ uliftFunctor))
      ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max u' w))) → Quot (F ⋙ uliftFunctor))
          ((AddEquiv.symm AddEquiv.ulift : (a : (↑(F.obj j) : Type w)) → ULift.{u', w} (↑(F.obj j) : Type w)) a) :
        Quot (F ⋙ uliftFunctor))
      ((AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) :
            (a : (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
          a :
        Quot (F ⋙ uliftFunctor)) =
    0
⊢ HSub.hSub (α := Quot (F ⋙ uliftFunctor)) (β := Quot (F ⋙ uliftFunctor))
      ((Quot.ι (F ⋙ uliftFunctor) j' : (a : (↑((F ⋙ uliftFunctor).obj j') : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max w u')) →+ (↑x2 : Type (max w u'))) (CC := carrier) ((F ⋙ uliftFunctor).map u) :
              (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → (↑((F ⋙ uliftFunctor).obj j') : Type (max w u')))
            ((AddEquiv.symm AddEquiv.ulift : (a : (↑(F.obj j) : Type w)) → ULift.{u', w} (↑(F.obj j) : Type w)) a)) :
        Quot (F ⋙ uliftFunctor))
      ((AddMonoidHom.comp (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) :
            (a : (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
          a :
        Quot (F ⋙ uliftFunctor)) =
    0

Tactic:
rw [Quot.map_ι]

Premises used: AddCommGrpCat.Colimits.Quot.map_ι
-- 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
j j' : J
u : j ⟶ j'
a : (↑(F.obj j) : Type w)
rw rw₁ : Eq (α := Quot (F ⋙ uliftFunctor)) 0 0
⊢ HSub.hSub (α := Quot (F ⋙ uliftFunctor)) (β := Quot (F ⋙ uliftFunctor))
      ((Quot.ι (F ⋙ uliftFunctor) j : (a : ULift.{u', w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
          ((AddEquiv.symm AddEquiv.ulift : (a : (↑(F.obj j) : Type w)) → ULift.{u', w} (↑(F.obj j) : Type w)) a) :
        Quot (F ⋙ uliftFunctor))
      ((Quot.ι (F ⋙ uliftFunctor) j : (a : ULift.{u', w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
          ((AddEquiv.symm AddEquiv.ulift : (a : (↑(F.obj j) : Type w)) → ULift.{u', w} (↑(F.obj j) : Type w)) a) :
        Quot (F ⋙ uliftFunctor)) =
    0

Tactic:
rw [sub_self]

Premises used: sub_self
-- 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
inst_1 : DecidableEq J
j : J
x : (↑(F.obj j) : Type w)
simp :
  Eq (α := Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
            (DFinsupp.singleAddHom (fun (j : J) ↦ ULift.{u_1, w} (↑(F.obj j) : Type w)) j) :
          (a : ULift.{u_1, w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
        ((AddEquiv.symm AddEquiv.ulift : (a : (↑(F.obj j) : Type w)) → ULift.{u_1, w} (↑(F.obj j) : Type w)) x) :
      Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
            (DFinsupp.singleAddHom (fun (j : J) ↦ ULift.{u_1, w} (↑(F.obj j) : Type w)) j) :
          (a : ULift.{u_1, w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
        { down := x } :
      Quot (F ⋙ uliftFunctor))
⊢ Eq (α := Quot (F ⋙ uliftFunctor))
    ((DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (j : J) ↦
            AddMonoidHom.comp
              (AddMonoidHom.comp (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
                (DFinsupp.singleAddHom (fun (j : J) ↦ ULift.{u_1, w} (↑(F.obj j) : Type w)) j))
              (↑(AddEquiv.symm AddEquiv.ulift) : (↑(F.obj j) : Type w) →+ ULift.{u_1, w} (↑(F.obj j) : Type w)) :
          (a : Π₀ (j : J), (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
        (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j :
              (↑(F.obj j) : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j) : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          x) :
      Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
            (DFinsupp.singleAddHom (fun (j : J) ↦ ULift.{u_1, w} (↑(F.obj j) : Type w)) j) :
          (a : ULift.{u_1, w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
        { down := x } :
      Quot (F ⋙ uliftFunctor))

Tactic:
simp only [DFinsupp.singleAddHom_apply, DFinsupp.sumAddHom_single, AddMonoidHom.coe_comp,
    AddMonoidHom.coe_coe, Function.comp_apply]

Premises used: DFinsupp.sumAddHom_single, AddMonoidHom.coe_coe, AddMonoidHom.coe_comp, Function.comp_apply, DFinsupp.singleAddHom_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
inst_1 : DecidableEq J
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
            (DFinsupp.singleAddHom (fun (j : J) ↦ ULift.{u_1, w} (↑(F.obj j) : Type w)) j) :
          (a : ULift.{u_1, w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
        ((AddEquiv.symm AddEquiv.ulift : (a : (↑(F.obj j) : Type w)) → ULift.{u_1, w} (↑(F.obj j) : Type w)) x) :
      Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
            (DFinsupp.singleAddHom (fun (j : J) ↦ ULift.{u_1, w} (↑(F.obj j) : Type w)) j) :
          (a : ULift.{u_1, w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor))
        { down := x } :
      Quot (F ⋙ uliftFunctor))

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
refine :
  Relations (F ⋙ uliftFunctor) ≤
    AddMonoidHom.ker (M := Quot F)
      (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) fun (j : J) ↦
        AddMonoidHom.comp (Quot.ι F j) (AddEquiv.toAddMonoidHom AddEquiv.ulift))
⊢ Quot (F ⋙ uliftFunctor) →+ Quot F

Tactic:
refine QuotientAddGroup.lift (Relations (F ⋙ uliftFunctor))
    (DFinsupp.sumAddHom (fun j ↦ (Quot.ι _ j).comp AddEquiv.ulift.toAddMonoidHom)) ?_

Premises used: AddCommGrpCat.uliftFunctor, AddEquiv.toAddMonoidHom, CategoryTheory.Functor.comp, AddCommGrpCat.Colimits.Quot.ι, DFinsupp.sumAddHom, AddCommGrpCat.Colimits.Relations, AddMonoidHom.comp, QuotientAddGroup.lift
-- 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
rw :
  {x : Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u')) |
      ∃ (j : J) (j' : J) (u : j ⟶ j') (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))),
        x =
          HSub.hSub (α := Π₀ (i : J), (↑((F ⋙ uliftFunctor).obj i) : Type (max w u')))
            (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j'
              ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max w u')) →+ (↑x2 : Type (max w u'))) (CC := carrier) ((F ⋙ uliftFunctor).map u) :
                  (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) →
                    (↑((F ⋙ uliftFunctor).obj j') : Type (max w u')))
                a))
            (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j a)} ⊆
    (↑(AddMonoidHom.ker (M := Quot F)
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) fun (j : J) ↦
            AddMonoidHom.comp (Quot.ι F j) (AddEquiv.toAddMonoidHom AddEquiv.ulift))) :
      Set (Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))))
⊢ Relations (F ⋙ uliftFunctor) ≤
    AddMonoidHom.ker (M := Quot F)
      (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) fun (j : J) ↦
        AddMonoidHom.comp (Quot.ι F j) (AddEquiv.toAddMonoidHom AddEquiv.ulift))

Tactic:
rw [AddSubgroup.closure_le]

Premises used: AddSubgroup.closure_le
-- 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 : Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))
hx :
  Membership.mem (γ := Set (Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))))
    {x : Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u')) |
      ∃ (j : J) (j' : J) (u : j ⟶ j') (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))),
        x =
          HSub.hSub (α := Π₀ (i : J), (↑((F ⋙ uliftFunctor).obj i) : Type (max w u')))
            (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j'
              ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max w u')) →+ (↑x2 : Type (max w u'))) (CC := carrier) ((F ⋙ uliftFunctor).map u) :
                  (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) →
                    (↑((F ⋙ uliftFunctor).obj j') : Type (max w u')))
                a))
            (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j a)}
    a
obtain :
  ∀ (j j' : J) (u : j ⟶ j') (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))),
    HSub.hSub (α := Π₀ (i : J), (↑((F ⋙ uliftFunctor).obj i) : Type (max w u')))
        (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j'
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max w u')) →+ (↑x2 : Type (max w u'))) (CC := carrier) ((F ⋙ uliftFunctor).map u) :
              (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → (↑((F ⋙ uliftFunctor).obj j') : Type (max w u')))
            a))
        (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j a) ∈
      (↑(AddMonoidHom.ker (M := Quot F)
            (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) fun (j : J) ↦
              AddMonoidHom.comp (Quot.ι F j) (AddEquiv.toAddMonoidHom AddEquiv.ulift))) :
        Set (Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))))
⊢ a ∈
    (↑(AddMonoidHom.ker (M := Quot F)
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) fun (j : J) ↦
            AddMonoidHom.comp (Quot.ι F j) (AddEquiv.toAddMonoidHom AddEquiv.ulift))) :
      Set (Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))))

Tactic:
obtain ⟨j, j', u, a, rfl⟩ := hx

Premises used: 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
j j' : J
u : j ⟶ j'
a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))
⊢ HSub.hSub (α := Π₀ (i : J), (↑((F ⋙ uliftFunctor).obj i) : Type (max w u')))
      (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max w u')) →+ (↑x2 : Type (max w u')))
              (CC := carrier) ((F ⋙ uliftFunctor).map u) :
            (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → (↑((F ⋙ uliftFunctor).obj j') : Type (max w u')))
          a))
      (DFinsupp.single (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j a) ∈
    (↑(AddMonoidHom.ker (M := Quot F)
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) fun (j : J) ↦
            AddMonoidHom.comp (Quot.ι F j) (AddEquiv.toAddMonoidHom AddEquiv.ulift))) :
      Set (Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))))

Tactic:
simp