-- 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)
refine_1 :
  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))))
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (ULift.down.{w, 0}
      ((Hom.hom
            (c.ι.app j ≫
              (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 : (↑(F.obj j) : Type w)) → (↑(of (ULift.{w, 0} (AddCircle 1))) : Type w))
        x))
    (ULift.down.{w, 0}
      ((Hom.hom
            (c.ι.app j ≫
              (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 : (↑(F.obj j) : Type w)) → (↑(of (ULift.{w, 0} (AddCircle 1))) : Type w))
        x))

Tactic:
rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ← Quot.ι_desc _ c j x]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, AddCommGrpCat.Colimits.Quot.ι_desc