awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑c.pt : Type w))
    ((desc F c : (a : Quot F) → (↑c.pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) : (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (c.ι.app j) :
          (a : (↑(F.obj j) : Type w)) → (↑(((Functor.const J).obj c.pt).obj j) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j) : Type w))
have dsimp : Eq.{w + 1} (α := (↑c.pt : Type w))
  ((QuotientAddGroup.lift (Relations F)
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x)) sorry :
        (a : Quot F) → (↑c.pt : Type w))
      ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
          (a : (↑(F.obj j) : Type w)) → Quot F)
        x) :
    (↑c.pt : Type w))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
          (c.ι.app j) :
        (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w))
      x :
    (↑c.pt : Type w))
Tactic: dsimp [desc, ι]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑c.pt : Type w))
    ((QuotientAddGroup.lift (Relations F)
            (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x)) ⋯ :
          (a : Quot F) → (↑c.pt : Type w))
        ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
            (a : (↑(F.obj j) : Type w)) → Quot F)
          x) :
      (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (c.ι.app j) :
          (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w))
        x :
      (↑c.pt : Type w))
have erw : Eq.{w + 1} (α := (↑c.pt : Type w))
  ((DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x) :
        (a : Π₀ (j : J), (↑(F.obj j) : Type w)) → (↑c.pt : 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) :
    (↑c.pt : Type w))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
          (c.ι.app j) :
        (a : (↑(F.obj j) : Type w)) → (↑c.pt : Type w))
      x :
    (↑c.pt : Type w))
Tactic: erw [QuotientAddGroup.lift_mk']
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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)
⊢ Eq (α := Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j') :
          (a : (↑(F.obj j') : Type w)) → Quot F)
        ((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) :
      Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
          (a : (↑(F.obj j) : Type w)) → Quot F)
        x :
      Quot F)
have refine : HSub.hSub (α := Quot F) (β := Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j') :
          (a : (↑(F.obj j') : Type w)) → Quot F)
        ((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) :
      Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
          (a : (↑(F.obj j) : Type w)) → Quot F)
        x :
      Quot F) =
  0
Tactic: refine eq_of_sub_eq_zero ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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 (α := Quot F) (β := Quot F)
      ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j') :
            (a : (↑(F.obj j') : Type w)) → Quot F)
          ((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) :
        Quot F)
      ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
            (a : (↑(F.obj j) : Type w)) → Quot F)
          x :
        Quot F) =
    0
have erw : 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)) ∈
  AddMonoidHom.ker (QuotientAddGroup.mk' (Relations F))
Tactic: erw [← (QuotientAddGroup.mk' (Relations F)).map_sub, ← AddMonoidHom.mem_ker]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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)) (β := Π₀ (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)) ∈
    AddMonoidHom.ker (QuotientAddGroup.mk' (Relations F))
have rw : 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: rw [QuotientAddGroup.ker_mk']
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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)) (β := Π₀ (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
have 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
Tactic: simp only [DFinsupp.singleAddHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [AddSubgroup.closure_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
⊢ 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)))
have 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)))
Tactic: obtain ⟨j, j', u, a, rfl⟩ := hx
Cleared hypotheses: a, hx
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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)
⊢ 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)))
have 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
Tactic: rw [SetLike.mem_coe, AddMonoidHom.mem_ker, map_sub, DFinsupp.sumAddHom_single,
    DFinsupp.sumAddHom_single]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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)
⊢ 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
have 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
Tactic: change Quot.ι (F ⋙ uliftFunctor) j' ((F ⋙ uliftFunctor).map u (AddEquiv.ulift.symm a)) - _ = _
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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)
⊢ 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
have 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
Tactic: rw [Quot.map_ι]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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)
⊢ 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
have rw : Eq (α := Quot (F ⋙ uliftFunctor)) 0 0
Tactic: rw [sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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))
    ((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))
have 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))
Tactic: simp only [DFinsupp.singleAddHom_apply, DFinsupp.sumAddHom_single, AddMonoidHom.coe_comp,
    AddMonoidHom.coe_coe, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Colimits (goal)
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
⊢ Quot (F ⋙ uliftFunctor) →+ Quot F
have 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))
Tactic: refine QuotientAddGroup.lift (Relations (F ⋙ uliftFunctor))
    (DFinsupp.sumAddHom (fun j ↦ (Quot.ι _ j).comp AddEquiv.ulift.toAddMonoidHom)) ?_