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
x : (↑((F ⋙ uliftFunctor).obj j) : Type (max u' w))
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)
⊢ 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)

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

Premises used: CategoryTheory.Functor.comp_obj, DFinsupp.sumAddHom_single, AddMonoidHom.coe_coe, AddCommGrpCat.uliftFunctor_obj, 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 ⋙ uliftFunctor).obj j) : Type (max u' 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)
        ((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:
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
x : Quot F
rw : ((AddMonoidHom.id (Quot F) : (a : Quot F) → Quot F) x : Quot F)
| x

Tactic:
rw [← AddMonoidHom.id_apply _ x]

Premises used: AddMonoidHom.id_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
x : Quot F
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)
⊢ (quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F)
      ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor)) x) =
    x

Tactic:
conv_rhs => rw [← AddMonoidHom.id_apply _ x]

Premises used: AddMonoidHom.id_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
x : Quot F
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)
⊢ 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:
rw [← AddMonoidHom.comp_apply, Quot.addMonoidHom_ext F (f := (quotUliftToQuot F).comp
      (quotToQuotUlift F)) (fun j a ↦ ?_)]

Premises used: AddCommGrpCat.Colimits.Quot.addMonoidHom_ext, AddMonoidHom.comp_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
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)
rw₃ 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)
⊢ 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, AddMonoidHom.id_apply, quotToQuotUlift_ι, quotUliftToQuot_ι]

Premises used: AddMonoidHom.id_apply, AddCommGrpCat.Colimits.quotUliftToQuot_ι, AddCommGrpCat.Colimits.quotToQuotUlift_ι, AddMonoidHom.comp_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
x : Quot (F ⋙ uliftFunctor)
rw :
  ((AddMonoidHom.id (Quot (F ⋙ uliftFunctor)) : (a : Quot (F ⋙ uliftFunctor)) → Quot (F ⋙ uliftFunctor)) x :
    Quot (F ⋙ uliftFunctor))
| x

Tactic:
rw [← AddMonoidHom.id_apply _ x]

Premises used: AddMonoidHom.id_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
x : Quot (F ⋙ uliftFunctor)
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))
⊢ (quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor))
      ((quotUliftToQuot F : (a : Quot (F ⋙ uliftFunctor)) → Quot F) x) =
    x

Tactic:
conv_rhs => rw [← AddMonoidHom.id_apply _ x]

Premises used: AddMonoidHom.id_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
x : Quot (F ⋙ uliftFunctor)
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))
⊢ 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:
rw [← AddMonoidHom.comp_apply, Quot.addMonoidHom_ext _ (f := (quotToQuotUlift F).comp
      (quotUliftToQuot F)) (fun j a ↦ ?_)]

Premises used: AddCommGrpCat.Colimits.Quot.addMonoidHom_ext, AddMonoidHom.comp_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
x : Quot (F ⋙ uliftFunctor)
j : J
a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))
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))
⊢ 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, AddMonoidHom.id_apply, quotUliftToQuot_ι, quotToQuotUlift_ι]

Premises used: AddMonoidHom.id_apply, AddCommGrpCat.Colimits.quotUliftToQuot_ι, AddCommGrpCat.Colimits.quotToQuotUlift_ι, AddMonoidHom.comp_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
x : Quot (F ⋙ uliftFunctor)
j : J
a : (↑((F ⋙ uliftFunctor).obj j) : Type (max w u'))
⊢ 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:
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
x x_1 : Quot F
⊢ (quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor)) (x + x_1) =
    HAdd.hAdd (α := Quot (F ⋙ uliftFunctor)) (β := Quot (F ⋙ uliftFunctor))
      ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor)) x : Quot (F ⋙ uliftFunctor))
      ((quotToQuotUlift F : (a : Quot F) → Quot (F ⋙ uliftFunctor)) x_1 : Quot (F ⋙ uliftFunctor))

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
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))

Tactic:
Quot.addMonoidHom_ext _ (fun j a ↦ ?_)

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
inst_1 : DecidableEq J
c : Cocone F
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)))
⊢ 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))

Tactic:
refine Quot.addMonoidHom_ext _ (fun j a ↦ ?_)

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
inst_1 : DecidableEq J
c : Cocone F
j : J
a : (↑(F.obj j) : Type w)
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))
⊢ 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))

Tactic:
simp only [quotToQuotUlift_ι, Functor.comp_obj, uliftFunctor_obj, ι_desc, Functor.const_obj_obj,
    ι_desc]

Premises used: CategoryTheory.Functor.comp_obj, AddCommGrpCat.Colimits.quotToQuotUlift_ι, AddCommGrpCat.Colimits.Quot.ι_desc, AddCommGrpCat.uliftFunctor_obj, 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
inst_1 : DecidableEq J
c : Cocone F
j : J
a : (↑(F.obj j) : Type w)
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))
⊢ 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:
erw [Quot.ι_desc]

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
inst_1 : DecidableEq J
c : Cocone F
j : J
a : (↑(F.obj j) : Type w)
⊢ 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:
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
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

Tactic:
Quot.addMonoidHom_ext F (fun j x ↦ ?_)

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
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
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))
⊢ AddMonoidHom.comp (Hom.hom (hc.desc (toCocone F f))) (desc F c) = f

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)

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
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))
    ((Hom.hom (hc.desc (toCocone F f)) : (a : (↑c.pt : Type w)) → (↑(toCocone F f).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)) :
      (↑(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.{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:
rw [AddMonoidHom.comp_apply, ι_desc]

Premises used: AddCommGrpCat.Colimits.Quot.ι_desc, AddMonoidHom.comp_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
A : Type w
inst_2 : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : (↑(F.obj j) : Type w)
change :
  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))
⊢ Eq (α := (↑(toCocone F f).pt : Type w))
    ((Hom.hom (hc.desc (toCocone F f)) : (a : (↑c.pt : Type w)) → (↑(toCocone F f).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)) :
      (↑(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:
change (c.ι.app j ≫ hc.desc (toCocone F f)) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, AddCommGrpCat.Colimits.toCocone, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app