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
⊢ 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))
have 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'))))
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 ⋙ 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
⊢ 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'))))
have 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'))))
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
inst_1 : DecidableEq J
j : J
x : (↑((F ⋙ uliftFunctor).obj j) : Type (max u' w))
⊢ Eq (α := Quot F)
    ((DFinsupp.sumAddHom (β := fun (j : J) ↦ ULift.{u', w} (↑(F.obj j) : Type w)) fun (j : J) ↦
            AddMonoidHom.comp
              (AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
                (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j))
              (↑AddEquiv.ulift : ULift.{u', w} (↑(F.obj j) : Type w) →+ (↑(F.obj j) : Type w)) :
          (a : Π₀ (j : J), ULift.{u', w} (↑(F.obj j) : Type w)) → Quot F)
        (((DFinsupp.singleAddHom (fun (j : J) ↦ (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) j :
              (↑((F ⋙ uliftFunctor).obj j) : Type (max w u')) →+
                Π₀ (i : J), (↑((F ⋙ uliftFunctor).obj i) : Type (max w u'))) :
            (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) →
              Π₀ (j : J), (↑((F ⋙ uliftFunctor).obj j) : Type (max w u')))
          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.down :
      Quot F)
have simp : 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)
      ((AddEquiv.ulift : (a : ULift.{u', w} (↑(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.down :
    Quot F)
Tactic: simp only [Functor.comp_obj, uliftFunctor_obj, 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
x : Quot F
| x
have rw : ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) x : Quot F)
Tactic: rw [← AddMonoidHom.id_apply _ x]
-- 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
x : Quot F
⊢ (quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
      ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor)) x) =
    x
have conv_rhs : Eq (α := Quot F)
  ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
      ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor)) x) :
    Quot F)
  ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) x : Quot F)
Tactic: conv_rhs => rw [← AddMonoidHom.id_apply _ x]
-- 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
x : Quot F
⊢ Eq (α := Quot F)
    ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
        ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor)) x) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) x : Quot F)
have rw : ∀ (j : J) (a : (↑(F.obj j) : Type w)),
  Eq (α := Quot F)
    ((AddMonoidHom.comp (quotUliftToQuot F) (quotToQuotUlift F) : (a : Quot F) → Quot F)
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
Tactic: rw [← AddMonoidHom.comp_apply, Quot.addMonoidHom_ext F (f := (quotUliftToQuot F).comp
      (quotToQuotUlift F)) (fun j 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
x : Quot F
j : J
a : (↑(F.obj j) : Type w)
⊢ Eq (α := Quot F)
    ((AddMonoidHom.comp (quotUliftToQuot F) (quotToQuotUlift F) : (a : Quot F) → Quot F)
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
have rw : Eq (α := Quot F)
  ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
      ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
    Quot F)
  ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) : Quot F)
Tactic: rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotToQuotUlift_ι, quotUliftToQuot_ι]
-- 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
x : Quot F
j : J
a : (↑(F.obj j) : Type w)
rw :
  Eq (α := Quot F)
    ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
        ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
          ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
⊢ Eq (α := Quot F)
    ((AddMonoidHom.comp (quotUliftToQuot F) (quotToQuotUlift F) : (a : Quot F) → Quot F)
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
have rw₁ : Eq (α := Quot F)
  ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
      ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
    Quot F)
  ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a : Quot F)
Tactic: rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotToQuotUlift_ι, quotUliftToQuot_ι]
-- 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
x : Quot F
j : J
a : (↑(F.obj j) : Type w)
rw :
  Eq (α := Quot F)
    ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
        ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
          ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
rw₁ :
  Eq (α := Quot F)
    ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
        ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
          ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
      Quot F)
    ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a : Quot F)
⊢ Eq (α := Quot F)
    ((AddMonoidHom.comp (quotUliftToQuot F) (quotToQuotUlift F) : (a : Quot F) → Quot F)
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
have rw₂ : Eq (α := Quot F)
  ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
      ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
        { down := a }) :
    Quot F)
  ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a : Quot F)
Tactic: rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotToQuotUlift_ι, quotUliftToQuot_ι]
-- 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
x : Quot F
j : J
a : (↑(F.obj j) : Type w)
rw :
  Eq (α := Quot F)
    ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
        ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
          ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
rw₁ :
  Eq (α := Quot F)
    ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
        ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
          ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
      Quot F)
    ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a : Quot F)
rw₂ :
  Eq (α := Quot F)
    ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
        ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
          { down := a }) :
      Quot F)
    ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a : Quot F)
⊢ Eq (α := Quot F)
    ((AddMonoidHom.comp (quotUliftToQuot F) (quotToQuotUlift F) : (a : Quot F) → Quot F)
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
    ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      Quot F)
have rw₃ : Eq (α := Quot F) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) (ULift.down.{u', w} { down := a }) : Quot F)
  ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a : Quot F)
Tactic: rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotToQuotUlift_ι, quotUliftToQuot_ι]
-- 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
x : Quot (F ⋙ uliftFunctor)
| x
have rw : ((AddMonoidHom.id (Quot (F ⋙ uliftFunctor)) : (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor)) x :
  Quot (F ⋙ uliftFunctor))
Tactic: rw [← AddMonoidHom.id_apply _ x]
-- 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
x : Quot (F ⋙ uliftFunctor)
⊢ (quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
      ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F) x) =
    x
have conv_rhs : Eq (α := Quot (F ⋙ uliftFunctor))
  ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
      ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F) x) :
    Quot (F ⋙ uliftFunctor))
  ((AddMonoidHom.id (Quot (F ⋙ uliftFunctor)) : (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor)) x :
    Quot (F ⋙ uliftFunctor))
Tactic: conv_rhs => rw [← AddMonoidHom.id_apply _ x]
-- 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
x : Quot (F ⋙ uliftFunctor)
⊢ Eq (α := Quot (F ⋙ uliftFunctor))
    ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
        ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F) x) :
      Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.id (Quot (F ⋙ uliftFunctor)) : (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor)) x :
      Quot (F ⋙ uliftFunctor))
have rw : ∀ (j : J) (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))),
  Eq (α := Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.comp (quotToQuotUlift F) (quotUliftToQuot F) :
          (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor))
        ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
          a) :
      Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.id (Quot (F ⋙ uliftFunctor)) : (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor))
        ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
          a) :
      Quot (F ⋙ uliftFunctor))
Tactic: rw [← AddMonoidHom.comp_apply, Quot.addMonoidHom_ext _ (f := (quotToQuotUlift F).comp
      (quotUliftToQuot F)) (fun j 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
x : Quot (F ⋙ uliftFunctor)
j : J
a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))
⊢ Eq (α := Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.comp (quotToQuotUlift F) (quotUliftToQuot F) :
          (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor))
        ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
          a) :
      Quot (F ⋙ uliftFunctor))
    ((AddMonoidHom.id (Quot (F ⋙ uliftFunctor)) : (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor))
        ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
          a) :
      Quot (F ⋙ uliftFunctor))
have rw : Eq (α := Quot (F ⋙ uliftFunctor))
  ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor))
      { down := a.down } :
    Quot (F ⋙ uliftFunctor))
  ((Quot.ι (F ⋙ uliftFunctor) j : (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))) → Quot (F ⋙ uliftFunctor)) a :
    Quot (F ⋙ uliftFunctor))
Tactic: rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotUliftToQuot_ι, quotToQuotUlift_ι]
-- 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
c : Cocone F
⊢ Eq (α := Quot F →+ (↑(uliftFunctor.mapCocone c).pt : Type (max u' w)))
    (AddMonoidHom.comp (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c))
      (AddEquiv.toAddMonoidHom (quotQuotUliftAddEquiv F)))
    (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) (desc F c))
have refine : ∀ (j : J) (a : (↑(F.obj j) : Type w)),
  Eq (α := (↑(uliftFunctor.mapCocone c).pt : Type (max u' w)))
    ((AddMonoidHom.comp (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c))
            (AddEquiv.toAddMonoidHom (quotQuotUliftAddEquiv F)) :
          (a : Quot F) → (↑(uliftFunctor.mapCocone c).pt : Type (max u' w)))
        ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      (↑(uliftFunctor.mapCocone c).pt : Type (max u' w)))
    ((AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) (desc F c) :
          (a : Quot F) → (↑(uliftFunctor.mapCocone c).pt : Type (max u' w)))
        ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a) :
      (↑(uliftFunctor.mapCocone c).pt : Type (max u' w)))
Tactic: refine Quot.addMonoidHom_ext _ (fun j 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
inst_1 : DecidableEq J
c : Cocone F
j : J
a : (↑(F.obj j) : Type w)
⊢ Eq (α := ULift.{u', w} (↑c.pt : Type w))
    (((desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c) :
            Quot (F ⋙ uliftFunctor) →+ (↑(uliftFunctor.mapCocone c).pt : Type (max u' w))) :
          (a : Quot (F ⋙ uliftFunctor)) → ULift.{u', w} (↑c.pt : Type w))
        ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
          ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
      ULift.{u', w} (↑c.pt : Type w))
    ((AddEquiv.symm AddEquiv.ulift : (a : (↑c.pt : Type w)) → ULift.{u', w} (↑c.pt : Type w))
        ((desc F c : (a : Quot F) → (↑c.pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) a)) :
      ULift.{u', w} (↑c.pt : Type w))
have simp : Eq (α := ULift.{u', w} (↑c.pt : Type w))
  (((desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c) :
          Quot (F ⋙ uliftFunctor) →+ (↑(uliftFunctor.mapCocone c).pt : Type (max u' w))) :
        (a : Quot (F ⋙ uliftFunctor)) → ULift.{u', w} (↑c.pt : Type w))
      ((ι (F ⋙ uliftFunctor) j : (a : ULift.{u', w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor)) { down := a }) :
    ULift.{u', w} (↑c.pt : Type w))
  ((AddEquiv.symm AddEquiv.ulift : (a : (↑c.pt : Type w)) → ULift.{u', w} (↑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))
        a) :
    ULift.{u', w} (↑c.pt : Type w))
Tactic: simp only [quotToQuotUlift_ι, Functor.comp_obj, uliftFunctor_obj, ι_desc, Functor.const_obj_obj,
    ι_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
inst_1 : DecidableEq J
c : Cocone F
j : J
a : (↑(F.obj j) : Type w)
⊢ Eq (α := ULift.{u', w} (↑c.pt : Type w))
    (((desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c) :
            Quot (F ⋙ uliftFunctor) →+ (↑(uliftFunctor.mapCocone c).pt : Type (max u' w))) :
          (a : Quot (F ⋙ uliftFunctor)) → ULift.{u', w} (↑c.pt : Type w))
        ((ι (F ⋙ uliftFunctor) j : (a : ULift.{u', w} (↑(F.obj j) : Type w)) → Quot (F ⋙ uliftFunctor)) { down := a }) :
      ULift.{u', w} (↑c.pt : Type w))
    ((AddEquiv.symm AddEquiv.ulift : (a : (↑c.pt : Type w)) → ULift.{u', w} (↑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))
          a) :
      ULift.{u', w} (↑c.pt : Type w))
have erw : Eq (α := ULift.{u', w} (↑c.pt : Type w))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u' w)) →+ (↑x2 : Type (max u' w))) (CC :=
          carrier) ((uliftFunctor.mapCocone c).ι.app j) :
        (a : (↑((F ⋙ uliftFunctor).obj j) : Type (max u' w))) →
          (↑(((Functor.const J).obj (uliftFunctor.mapCocone c).pt).obj j) : Type (max u' w)))
      { down := a } :
    (↑(Functor.obj (Functor.obj (Functor.const J) (uliftFunctor.mapCocone c).pt) j) : Type (max u' w)))
  ((AddEquiv.symm AddEquiv.ulift : (a : (↑c.pt : Type w)) → ULift.{u', w} (↑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))
        a) :
    ULift.{u', w} (↑c.pt : Type w))
Tactic: erw [Quot.ι_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
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
⊢ AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) = f
have refine : ∀ (j : J) (x : (↑(F.obj j) : Type w)),
  Eq.{w + 1} (α := (↑(toCocone F f).pt : Type w))
    ((AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) : (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))
    ((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: refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)