-- 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 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'))) = χ

Tactic:
refine Quot.addMonoidHom_ext _ (fun j x ↦ ?_)

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)
⊢ ((CharacterModule.dual (Quot.desc F c).toIntLinearMap) (AddEquiv.ulift.toAddMonoidHom.comp (Hom.hom (hc.desc c'))))
      ((Quot.ι F j) x) =
    χ ((Quot.ι F j) x)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(Quot.desc F c)

Tactic:
change Function.Bijective (Quot.desc F c).toIntLinearMap

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(Quot.desc F c).toIntLinearMap

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)
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ

Tactic:
set c' : Cocone F :=
  { pt := AddCommGrp.of (ULift (AddCircle (1 : ℚ)))
    ι :=
      { app j := AddCommGrp.ofHom (((@AddEquiv.ulift _ _).symm.toAddMonoidHom.comp χ).comp
                   (Quot.ι F j))
        naturality {j j'} u := by
          ext
          dsimp
          rw [Quot.map_ι F (f := u)] } }

Result:
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 = χ

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
⊢ Nonempty (IsColimit c) ↔ Function.Bijective ⇑(Quot.desc F c)

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

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(Quot.desc F c)

Proof state:
case refine_1
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) ψ
⊢ χ = ψ

Tactic:
apply (AddMonoidHom.postcompEquiv (@AddEquiv.ulift (AddCircle (1 : ℚ)) _).symm _).injective

Result:
case refine_1.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) ψ
⊢ (AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) χ = (AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) ψ

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(CharacterModule.dual (Quot.desc F c).toIntLinearMap)

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

Result:
case refine_1
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) ψ
⊢ χ = ψ

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)
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ

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) ψ
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) ψ)

Tactic:
ext 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)
⊢ ((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

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)
⊢ (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

Tactic:
exact DFunLike.congr_fun eq (Quot.ι F j x)

Result:
no goals

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 ((Hom.hom (hc.desc c')) ((Quot.desc F c) ((Quot.ι F j) x))) = χ ((Quot.ι F j) x)

Tactic:
rw [Quot.ι_desc]

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 ((Hom.hom (hc.desc c')) ((ConcreteCategory.hom (c.ι.app j)) x)) = χ ((Quot.ι F j) x)