awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
x₂ : (↑S.X₂ : Type u)
x₁ : (↑S.X₁ : Type u)
hx₁ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier) S.f :
        (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
      x₁ =
    x₂ -
      s
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂)
⊢ (fun (x : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)) ↦
        (match (motive := (↑S.X₁ : Type u) × (↑S.X₃ : Type u) → (↑S.X₂ : Type u)) x with
          | (x₁, x₃) =>
            HAdd.hAdd (α := (↑S.X₂ : Type u))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                      carrier) S.f :
                    (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
                  x₁ :
                (↑S.X₂ : Type u))
              (s x₃) :
          (↑S.X₂ : Type u)))
      (x₁,
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂) =
    x₂

Tactic:
simp [hx₁]
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
x₂ : (↑S.X₂ : Type u)
x₁ : (↑S.X₁ : Type u)
hx₁ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier) S.f :
        (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
      x₁ =
    x₂ -
      s
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂)
⊢ ∃ (a : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)),
    (fun (x : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)) ↦
          (match (motive := (↑S.X₁ : Type u) × (↑S.X₃ : Type u) → (↑S.X₂ : Type u)) x with
            | (x₁, x₃) =>
              HAdd.hAdd (α := (↑S.X₂ : Type u))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                        carrier) S.f :
                      (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
                    x₁ :
                  (↑S.X₂ : Type u))
                (s x₃) :
            (↑S.X₂ : Type u)))
        a =
      x₂

Tactic:
exact ⟨⟨x₁, S.g x₂⟩, by simp [hx₁]⟩
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
⊢ Function.Surjective (β := (↑S.X₂ : Type u)) fun (x : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)) ↦
    match (motive := (↑S.X₁ : Type u) × (↑S.X₃ : Type u) → (↑S.X₂ : Type u)) x with
    | (x₁, x₃) =>
      HAdd.hAdd (α := (↑S.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ :
          (↑S.X₂ : Type u))
        (s x₃)

Tactic:
have hφ : Function.Surjective (fun (x₁, x₃) ↦ S.f x₁ + s x₃) := fun x₂ ↦ by
      obtain ⟨x₁, hx₁⟩ := (ShortComplex.ab_exact_iff S).1 hS.exact (x₂ - s (S.g x₂))
        (by simp [hs (S.g x₂)])
      exact ⟨⟨x₁, S.g x₂⟩, by simp [hx₁]⟩
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
hφ :
  Function.Surjective (β := (↑S.X₂ : Type u)) fun (x : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)) ↦
    match (motive := (↑S.X₁ : Type u) × (↑S.X₃ : Type u) → (↑S.X₂ : Type u)) x with
    | (x₁, x₃) =>
      HAdd.hAdd (α := (↑S.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ :
          (↑S.X₂ : Type u))
        (s x₃)
⊢ Finite.{u + 1} (↑S.X₂ : Type u)

Tactic:
Finite.of_surjective _ hφ

Premises used: Finite.of_surjective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
hφ :
  Function.Surjective (β := (↑S.X₂ : Type u)) fun (x : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)) ↦
    match (motive := (↑S.X₁ : Type u) × (↑S.X₃ : Type u) → (↑S.X₂ : Type u)) x with
    | (x₁, x₃) =>
      HAdd.hAdd (α := (↑S.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ :
          (↑S.X₂ : Type u))
        (s x₃)
⊢ Finite.{u + 1} (↑S.X₂ : Type u)

Tactic:
exact Finite.of_surjective _ hφ

Premises used: Finite.of_surjective
-- Module: Mathlib.Algebra.Category.Grp.Kernels
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : Fork f 0
⊢ (fun (s : Fork f 0) ↦ ofHom ((Hom.hom s.ι).codRestrict (Hom.hom f).ker ⋯)) x ≫ Fork.ι (kernelCone f) = x.ι

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Kernels
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : Cofork f 0
x_1 : (cokernelCocone f).pt ⟶ x.pt
h : Cofork.π (cokernelCocone f) ≫ x_1 = x.π
this : Epi (Cofork.π (cokernelCocone f))
⊢ Cofork.π (cokernelCocone f) ≫ x_1 =
    Cofork.π (cokernelCocone f) ≫ (fun (s : Cofork f 0) ↦ ofHom (lift (Hom.hom f).range s.π.hom' ⋯)) x

Tactic:
simpa only [parallelPair_obj_one] using h

Premises used: CategoryTheory.Limits.parallelPair_obj_one
-- 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
⊢ Nonempty (IsColimit c) ↔
    Function.Bijective (α := Colimits.Quot F) (β := (↑c.pt : Type w))
      (⇑(Quot.desc F c) : (a : Colimits.Quot F) → (↑c.pt : Type w))

Tactic:
⟨fun ⟨hc⟩ => ?_, fun h ↦ Nonempty.intro (isColimit_of_bijective_desc F c h)⟩

Premises used: AddCommGrpCat.Colimits.isColimit_of_bijective_desc, Nonempty.intro, AddCommGrpCat.Colimits.Quot.desc, Iff.intro, Function.Bijective, DFunLike.coe, _private.0.AddCommGrpCat.isColimit_iff_bijective_desc.match_1
-- 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
refine :
  Nonempty (IsColimit c) →
    ∀ (hc : IsColimit c),
      Function.Bijective (α := Colimits.Quot F) (β := (↑c.pt : Type w))
        (⇑(Quot.desc F c) : (a : Colimits.Quot F) → (↑c.pt : Type w))
⊢ Nonempty (IsColimit c) ↔
    Function.Bijective (α := Colimits.Quot F) (β := (↑c.pt : Type w))
      (⇑(Quot.desc F c) : (a : Colimits.Quot F) → (↑c.pt : Type w))

Tactic:
refine ⟨fun ⟨hc⟩ => ?_, fun h ↦ Nonempty.intro (isColimit_of_bijective_desc F c h)⟩
-- 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
rw :
  Function.Bijective (α := CharacterModule (↑c.pt : Type w)) (β := CharacterModule (Colimits.Quot F))
    (⇑(CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c))) :
      (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
⊢ Function.Bijective (α := Colimits.Quot F) (β := (↑c.pt : Type w))
    (⇑(AddMonoidHom.toIntLinearMap (Quot.desc F c)) : (a : Colimits.Quot F) → (↑c.pt : Type w))

Tactic:
rw [← CharacterModule.dual_bijective_iff_bijective]

Premises used: CharacterModule.dual_bijective_iff_bijective
-- 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
⊢ Function.Bijective (α := CharacterModule (↑c.pt : Type w)) (β := CharacterModule (Colimits.Quot F))
    (⇑(CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c))) :
      (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))

Tactic:
⟨fun χ ψ eq ↦ ?_, fun χ ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- 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
refine_1 :
  ∀ (χ ψ : 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))),
    χ = ψ
refine_2 :
  ∀ (χ : CharacterModule (Colimits.Quot F)),
    ∃ (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 =
        χ
⊢ Function.Bijective (α := CharacterModule (↑c.pt : Type w)) (β := CharacterModule (Colimits.Quot F))
    (⇑(CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c))) :
      (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))

Tactic:
refine ⟨fun χ ψ eq ↦ ?_, fun χ ↦ ?_⟩
-- 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))
refine_1 :
  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))
⊢ χ = ψ

Tactic:
apply AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv.injective

Premises used: AddEquiv.addMonoidHomCongrRightEquiv, Equiv.injective
-- 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))
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))
        ψ))
⊢ 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))

Tactic:
apply ofHom_injective

Premises used: AddCommGrpCat.ofHom_injective
-- 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))
⊢ 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:
hc.hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_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 (↑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))
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))
            ψ))
⊢ 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:
refine hc.hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_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 (↑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
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))
⊢ 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:
ext x