-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (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
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}
      ((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))
have 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))))
Tactic: rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ← Quot.ι_desc _ c j x]