-- 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:
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

Tactic:
rw [← CharacterModule.dual_bijective_iff_bijective]

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 ⇑(CharacterModule.dual (Quot.desc F c).toIntLinearMap)

Proof state:
case hf.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)
j j' : J
u : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ AddEquiv.ulift.symm (χ ((Quot.ι F j') ((Hom.hom (F.map u)) x✝))) = AddEquiv.ulift.symm (χ ((Quot.ι F j) x✝))

Tactic:
rw [Quot.map_ι F (f := u)]

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

Tactic:
change AddEquiv.ulift ((c.ι.app j ≫ hc.desc c') 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)
⊢ AddEquiv.ulift ((ConcreteCategory.hom (c.ι.app j ≫ hc.desc c')) x) = χ ((Quot.ι F j) x)

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

Tactic:
rw [hc.fac]

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

Proof state:
case hf.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)
j j' : J
u : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map u ≫ (fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j))) j')) x✝ =
    (Hom.hom
        ((fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j))) j ≫
          ((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).map u))
      x✝

Tactic:
dsimp

Result:
case hf.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)
j j' : J
u : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ AddEquiv.ulift.symm (χ ((Quot.ι F j') ((Hom.hom (F.map u)) x✝))) = AddEquiv.ulift.symm (χ ((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
χ : CharacterModule (Colimits.Quot F)
j j' : J
u : j ⟶ j'
⊢ F.map u ≫ (fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j))) j' =
    (fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j))) j ≫
      ((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).map u

Tactic:
ext

Result:
case hf.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)
j j' : J
u : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map u ≫ (fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j))) j')) x✝ =
    (Hom.hom
        ((fun j => ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j))) j ≫
          ((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).map u))
      x✝

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

Tactic:
dsimp

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

Proof state:
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) ψ

Tactic:
apply ofHom_injective

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) ψ
⊢ (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) χ) =
    (fun f => ofHom f) ((AddMonoidHom.postcompEquiv AddEquiv.ulift.symm ↑c.pt) ψ)