awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule (↑c.pt : Type w)
eq :
  Eq (α := CharacterModule (Colimits.Quot F))
    ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        χ :
      CharacterModule (Colimits.Quot F))
    ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        ψ :
      CharacterModule (Colimits.Quot F))
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (ULift.down.{w, 0}
      ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            carrier _ _ (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j)
            (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))
            ((fun (f : (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)) ↦ ofHom f)
              ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
                  (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
                χ)) :
          (a : (↑(((Functor.const J).obj c.pt).obj j) : Type w)) → (↑(of (ULift.{w, 0} (AddCircle 1))) : Type w))
        ((Quot.desc F c : (a : Colimits.Quot F) → (↑c.pt : Type w))
            ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          (↑c.pt : Type w))))
    (ULift.down.{w, 0}
      ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            carrier _ _ (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j)
            (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))
            ((fun (f : (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)) ↦ ofHom f)
              ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
                  (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
                ψ)) :
          (a : (↑(((Functor.const J).obj c.pt).obj j) : Type w)) → (↑(of (ULift.{w, 0} (AddCircle 1))) : Type w))
        ((Quot.desc F c : (a : Colimits.Quot F) → (↑c.pt : Type w))
            ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          (↑c.pt : Type w))))

Tactic:
DFunLike.congr_fun eq (Quot.ι F j x)

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, AddCommGrpCat.Colimits.Quot.ι, List.foldr, DFunLike.coe, Finset.sum, Trunc.lift
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule (↑c.pt : Type w)
eq :
  Eq (α := CharacterModule (Colimits.Quot F))
    ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        χ :
      CharacterModule (Colimits.Quot F))
    ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        ψ :
      CharacterModule (Colimits.Quot F))
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (ULift.down.{w, 0}
      ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            carrier _ _ (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j)
            (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))
            ((fun (f : (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)) ↦ ofHom f)
              ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
                  (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
                χ)) :
          (a : (↑(((Functor.const J).obj c.pt).obj j) : Type w)) → (↑(of (ULift.{w, 0} (AddCircle 1))) : Type w))
        ((Quot.desc F c : (a : Colimits.Quot F) → (↑c.pt : Type w))
            ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          (↑c.pt : Type w))))
    (ULift.down.{w, 0}
      ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            carrier _ _ (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j)
            (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))
            ((fun (f : (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)) ↦ ofHom f)
              ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
                  (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
                ψ)) :
          (a : (↑(((Functor.const J).obj c.pt).obj j) : Type w)) → (↑(of (ULift.{w, 0} (AddCircle 1))) : Type w))
        ((Quot.desc F c : (a : Colimits.Quot F) → (↑c.pt : Type w))
            ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          (↑c.pt : Type w))))

Tactic:
exact DFunLike.congr_fun eq (Quot.ι F j x)

Premises used: DFunLike.congr_fun, AddCommGrpCat.Colimits.Quot.ι, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
j j' : J
u : j ⟶ j'
hf :
  ∀ (x : (↑(F.obj j) : Type w)),
    Eq (α :=
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j') :
        Type w))
      ((Hom.hom
              (F.map u ≫
                ofHom
                  (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
                    (Quot.ι F j'))) :
            (a : (↑(F.obj j) : Type w)) →
              (↑(((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).obj j') : Type w))
          x :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j') :
          Type w))
      ((Hom.hom
              (ofHom
                  (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
                    (Quot.ι F j)) ≫
                CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))))
                  u) :
            (a : (↑(F.obj j) : Type w)) →
              (↑(((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).obj j') : Type w))
          x :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j') :
          Type w))
⊢ Eq (α :=
    F.obj j ⟶
      Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j')
    (F.map u ≫
        ofHom
          (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
            (Quot.ι F j')) :
      F.obj j ⟶
        Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j')
    (ofHom
          (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
            (Quot.ι F j)) ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) u :
      F.obj j ⟶
        Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j')

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
j j' : J
u : j ⟶ j'
x : (↑(F.obj j) : Type w)
hf :
  Eq.{w + 1} (α := ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
        ((χ : (a : Colimits.Quot F) → AddCircle 1)
            ((Quot.ι F j' : (a : (↑(F.obj j') : Type w)) → Colimits.Quot F)
              ((Hom.hom (F.map u) : (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w)) x)) :
          AddCircle (𝕜 := ℚ) 1) :
      ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
        ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          AddCircle (𝕜 := ℚ) 1) :
      ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
⊢ Eq (α :=
    (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j') :
      Type w))
    ((Hom.hom
            (F.map u ≫
              ofHom
                (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
                  (Quot.ι F j'))) :
          (a : (↑(F.obj j) : Type w)) → (↑(((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).obj j') : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j') :
        Type w))
    ((Hom.hom
            (ofHom
                (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
                  (Quot.ι F j)) ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) u) :
          (a : (↑(F.obj j) : Type w)) → (↑(((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).obj j') : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) (of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))) j') :
        Type w))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
j j' : J
u : j ⟶ j'
x : (↑(F.obj j) : Type w)
hf hf₁ :
  Eq.{w + 1} (α := ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
        ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          AddCircle (𝕜 := ℚ) 1) :
      ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
        ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          AddCircle (𝕜 := ℚ) 1) :
      ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
⊢ Eq.{w + 1} (α := ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
        ((χ : (a : Colimits.Quot F) → AddCircle 1)
            ((Quot.ι F j' : (a : (↑(F.obj j') : Type w)) → Colimits.Quot F)
              ((Hom.hom (F.map u) : (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w)) x)) :
          AddCircle (𝕜 := ℚ) 1) :
      ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
        ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          AddCircle (𝕜 := ℚ) 1) :
      ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))

Tactic:
rw [Quot.map_ι F (f := u)]

Premises used: AddCommGrpCat.Colimits.Quot.map_ι
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
h :
  (CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
        (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
      (AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddEquiv.ulift) (Hom.hom (hc.desc c'))) =
    χ
⊢ ∃ (a : CharacterModule (↑c.pt : Type w)),
    (CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        a =
      χ

Tactic:
use AddEquiv.ulift.toAddMonoidHom.comp (hc.desc c').hom

Premises used: AddEquiv.toAddMonoidHom, CategoryTheory.Limits.IsColimit.desc, AddCommGrpCat.Hom.hom, AddMonoidHom.comp
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
⊢ (CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
        (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
      (AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddEquiv.ulift) (Hom.hom (hc.desc c'))) =
    χ

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

Premises used: AddCommGrpCat.Colimits.Quot.addMonoidHom_ext, CharacterModule
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
h :
  ∀ (j : J) (x : (↑(F.obj j) : Type w)),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
                  (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
                (AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddEquiv.ulift) (Hom.hom (hc.desc c'))) :
              CharacterModule (Colimits.Quot F)) :
            (a : Colimits.Quot F) → AddCircle 1)
          ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
        AddCircle (𝕜 := ℚ) 1)
      ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
        AddCircle (𝕜 := ℚ) 1)
⊢ (CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
        (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
      (AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddEquiv.ulift) (Hom.hom (hc.desc c'))) =
    χ

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

Premises used: AddCommGrpCat.Colimits.Quot.addMonoidHom_ext
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : (↑c'.pt : Type w)) → AddCircle 1)
        ((Hom.hom (hc.desc c') : (a : (↑c.pt : Type w)) → (↑c'.pt : Type w))
          ((Quot.desc F c : (a : Colimits.Quot F) → (↑c.pt : Type w))
              ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
            (↑c.pt : Type w))) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
                (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
              (AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddEquiv.ulift) (Hom.hom (hc.desc c'))) :
            CharacterModule (Colimits.Quot F)) :
          (a : Colimits.Quot F) → AddCircle 1)
        ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : (↑c'.pt : Type w)) → AddCircle 1)
        ((Hom.hom (hc.desc c') : (a : (↑c.pt : Type 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)) → (↑(((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))) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : (↑c'.pt : Type w)) → AddCircle 1)
        ((Hom.hom (hc.desc c') : (a : (↑c.pt : Type w)) → (↑c'.pt : Type w))
          ((Quot.desc F c : (a : Colimits.Quot F) → (↑c.pt : Type w))
              ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
            (↑c.pt : Type w))) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
rw [Quot.ι_desc]

Premises used: AddCommGrpCat.Colimits.Quot.ι_desc
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (c.ι.app j ≫ hc.desc c') :
            (a : (↑(F.obj j) : Type w)) → (↑c'.pt : Type w))
          x) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : (↑c'.pt : Type w)) → AddCircle 1)
        ((Hom.hom (hc.desc c') : (a : (↑c.pt : Type 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)) → (↑(((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))) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
change AddEquiv.ulift ((c.ι.app j ≫ hc.desc c') x) = _

Premises used: CategoryTheory.ConcreteCategory.hom, AddEquiv.ulift, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((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) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (c.ι.app j ≫ hc.desc c') :
            (a : (↑(F.obj j) : Type w)) → (↑c'.pt : Type w))
          x) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
rw [hc.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac