awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ Eq (α := (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
          (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
        χ :
      (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
    ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
          (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
        ψ :
      (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
have refine_1 : Eq.{w + 1} (α := of (↑c.pt : Type w) ⟶ 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))
      χ))
  ((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))
      ψ))
Tactic: apply ofHom_injective
-- 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))
⊢ Eq.{w + 1} (α := of (↑c.pt : Type w) ⟶ 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))
        χ))
    ((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))
        ψ))
have refine_1 : ∀ (j : J),
  Eq (α := F.obj j ⟶ of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))
    (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))
          χ))
    (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))
          ψ))
Tactic: refine hc.hom_ext (fun j ↦ ?_)
-- 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
⊢ Eq (α := F.obj j ⟶ of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)))
    (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))
          χ))
    (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))
          ψ))
have refine_1 : ∀ (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))
Tactic: ext x
-- 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 (Colimits.Quot F)
j j' : J
u : j ⟶ j'
⊢ 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')
have 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))
Tactic: ext
-- 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 (Colimits.Quot F)
j j' : J
u : j ⟶ j'
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))
have 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))
Tactic: dsimp
-- 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 (Colimits.Quot F)
j j' : J
u : j ⟶ j'
x : (↑(F.obj j) : Type w)
⊢ 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))
have 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))
Tactic: rw [Quot.map_ι F (f := u)]
-- 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 (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 := ⋯ } }
⊢ ∃ (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 =
      χ
have 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'))) =
  χ
Tactic: use AddEquiv.ulift.toAddMonoidHom.comp (hc.desc c').hom
-- 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 (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'))) =
    χ
have 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)
Tactic: refine Quot.addMonoidHom_ext _ (fun j x ↦ ?_)
-- 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 (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)
⊢ 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)
have 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)
Tactic: dsimp
-- 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 (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)
⊢ 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)
have 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)
Tactic: rw [Quot.ι_desc]
-- 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 (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)
⊢ 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)
have 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)
Tactic: change AddEquiv.ulift ((c.ι.app j ≫ hc.desc c') x) = _
-- 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 (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)
⊢ 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)
have 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)
Tactic: rw [hc.fac]