-- Mathlib/Algebra/Category/Grp/LargeColimits.lean
/--
If `c` is a cocone of `F` such that `Quot.desc F c` is bijective, then `c` is a colimit
cocone of `F`.
-/
lemma isColimit_iff_bijective_desc [DecidableEq J] :
     Nonempty (IsColimit c) ↔ Function.Bijective (Quot.desc F c)

Proof state:
case refine_1.a.a
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
⊢ (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) χ) =
    (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) ψ)

Tactic:
refine hc.hom_ext (fun j ↦ ?_)

Result:
case refine_1.a.a
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
⊢ c.ι.app j ≫ (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) χ) =
    c.ι.app j ≫ (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) ψ)

Proof state:
case refine_1.a.a.hf.h.h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((Hom.hom (c.ι.app j ≫ (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) χ))) x).down =
    ((Hom.hom (c.ι.app j ≫ (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) ψ))) x).down

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

Result:
case refine_1.a.a.hf.h.h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((ConcreteCategory.hom ((fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) χ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down =
    ((ConcreteCategory.hom ((fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) ψ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down

Proof state:
case refine_1.a.a.hf.h.h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((ConcreteCategory.hom ((fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) χ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down =
    ((ConcreteCategory.hom ((fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) ψ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down

Tactic:
simp only [hom_ofHom, AddMonoidHom.postcompEquiv_apply, AddMonoidHom.comp_apply]

Result:
case refine_1.a.a.hf.h.h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ (AddEquiv.ulift.symm.toAddMonoidHom (χ ((Quot.desc F c) ((Quot.ι F j) x)))).down =
    (AddEquiv.ulift.symm.toAddMonoidHom (ψ ((Quot.desc F c) ((Quot.ι F j) x)))).down

Proof state:
case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift ((ConcreteCategory.hom (c'.ι.app j)) x) = χ ((Quot.ι F j) x)

Tactic:
dsimp [c']

Result:
case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift (AddEquiv.ulift.symm (χ ((Quot.ι F j) x))) = χ ((Quot.ι F j) x)

Proof state:
case refine_2
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ

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

Result:
case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
⊢ (CharacterModule.dual (Quot.desc F c).toIntLinearMap) (AddEquiv.ulift.toAddMonoidHom.comp (Hom.hom (hc.desc c'))) = χ

Proof state:
case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift (AddEquiv.ulift.symm (χ ((Quot.ι F j) x))) = χ ((Quot.ι F j) x)

Tactic:
rw [AddEquiv.apply_symm_apply]

Result:
no goals