[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
⊢ coconeFun F j 0 = 0
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
⊢ Setoid.r (Prequotient.of j 0) zero
[PROOFSTEP]
apply Relation.zero
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
⊢ ∀ (x y : ↑(F.obj j)),
    ZeroHom.toFun
        { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
        (x + y) =
      ZeroHom.toFun
          { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
          x +
        ZeroHom.toFun
          { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) } y
[PROOFSTEP]
intros
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ ZeroHom.toFun
      { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
      (x✝ + y✝) =
    ZeroHom.toFun
        { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
        x✝ +
      ZeroHom.toFun
        { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) } y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (x✝ + y✝)) (add (Prequotient.of j x✝) (Prequotient.of j y✝))
[PROOFSTEP]
apply Relation.add
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case w.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
[PROOFSTEP]
apply Relation.map
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(coconeMorphism F j) x
[PROOFSTEP]
rw [← cocone_naturality F f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(F.map f ≫ coconeMorphism F j') x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), Setoid.r a b → descFunLift F s a = descFunLift F s b
[PROOFSTEP]
intro x y r
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction r with
| refl => rfl
| symm _ _ _ r_ih => exact r_ih.symm
| trans _ _ _ _ _ r_ih_h r_ih_k => exact Eq.trans r_ih_h r_ih_k
| map j j' f x => simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
| zero => simp
| neg => simp
| add => simp
| neg_1 _ _ _ r_ih => dsimp; rw [r_ih]
| add_1 _ _ _ _ r_ih => dsimp; rw [r_ih]
| add_2 _ _ _ _ r_ih => dsimp; rw [r_ih]
| zero_add => dsimp; rw [zero_add]
| add_zero => dsimp; rw [add_zero]
| add_left_neg => dsimp; rw [add_left_neg]
| add_comm => dsimp; rw [add_comm]
| add_assoc => dsimp; rw [add_assoc]
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction r with
| refl => rfl
| symm _ _ _ r_ih => exact r_ih.symm
| trans _ _ _ _ _ r_ih_h r_ih_k => exact Eq.trans r_ih_h r_ih_k
| map j j' f x => simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
| zero => simp
| neg => simp
| add => simp
| neg_1 _ _ _ r_ih => dsimp; rw [r_ih]
| add_1 _ _ _ _ r_ih => dsimp; rw [r_ih]
| add_2 _ _ _ _ r_ih => dsimp; rw [r_ih]
| zero_add => dsimp; rw [zero_add]
| add_zero => dsimp; rw [add_zero]
| add_left_neg => dsimp; rw [add_left_neg]
| add_comm => dsimp; rw [add_comm]
| add_assoc => dsimp; rw [add_assoc]
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]

| refl => rfl
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rfl
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
r_ih : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]

| symm _ _ _ r_ih => exact r_ih.symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
r_ih : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
exact r_ih.symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
r_ih_h : descFunLift F s x✝² = descFunLift F s y✝
r_ih_k : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]

| trans _ _ _ _ _ r_ih_h r_ih_k => exact Eq.trans r_ih_h r_ih_k
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
r_ih_h : descFunLift F s x✝² = descFunLift F s y✝
r_ih_k : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
exact Eq.trans r_ih_h r_ih_k
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' (↑(F.map f) x)) = descFunLift F s (Prequotient.of j x)
[PROOFSTEP]

| map j j' f x => simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' (↑(F.map f) x)) = descFunLift F s (Prequotient.of j x)
[PROOFSTEP]
simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
[GOAL]
case a.zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 0) = descFunLift F s zero
[PROOFSTEP]

| zero => simp
[GOAL]
case a.zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 0) = descFunLift F s zero
[PROOFSTEP]
simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (-x✝)) = descFunLift F s (neg (Prequotient.of j✝ x✝))
[PROOFSTEP]

| neg => simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (-x✝)) = descFunLift F s (neg (Prequotient.of j✝ x✝))
[PROOFSTEP]
simp
[GOAL]
case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ y✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (x✝ + y✝)) = descFunLift F s (add (Prequotient.of j✝ x✝) (Prequotient.of j✝ y✝))
[PROOFSTEP]

| add => simp
[GOAL]
case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ y✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (x✝ + y✝)) = descFunLift F s (add (Prequotient.of j✝ x✝) (Prequotient.of j✝ y✝))
[PROOFSTEP]
simp
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (neg x✝¹) = descFunLift F s (neg x'✝)
[PROOFSTEP]

| neg_1 _ _ _ r_ih => dsimp; rw [r_ih]
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (neg x✝¹) = descFunLift F s (neg x'✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ -descFunLift F s x✝¹ = -descFunLift F s x'✝
[PROOFSTEP]
rw [r_ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x'✝ y✝)
[PROOFSTEP]

| add_1 _ _ _ _ r_ih => dsimp; rw [r_ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x'✝ y✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s x✝¹ + descFunLift F s y✝ = descFunLift F s x'✝ + descFunLift F s y✝
[PROOFSTEP]
rw [r_ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
r_ih : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x✝¹ y'✝)
[PROOFSTEP]

| add_2 _ _ _ _ r_ih => dsimp; rw [r_ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
r_ih : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x✝¹ y'✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
r_ih : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s x✝¹ + descFunLift F s y✝ = descFunLift F s x✝¹ + descFunLift F s y'✝
[PROOFSTEP]
rw [r_ih]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]

| zero_add => dsimp; rw [zero_add]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]
dsimp
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ 0 + descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rw [zero_add]
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]

| add_zero => dsimp; rw [add_zero]
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]
dsimp
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ + 0 = descFunLift F s x✝
[PROOFSTEP]
rw [add_zero]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]

| add_left_neg => dsimp; rw [add_left_neg]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]
dsimp
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ -descFunLift F s x✝ + descFunLift F s x✝ = 0
[PROOFSTEP]
rw [add_left_neg]
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]

| add_comm => dsimp; rw [add_comm]
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s x✝ + descFunLift F s y✝ = descFunLift F s y✝ + descFunLift F s x✝
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (add (add x✝ y✝) z✝) = descFunLift F s (add x✝ (add y✝ z✝))
[PROOFSTEP]

| add_assoc => dsimp; rw [add_assoc]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (add (add x✝ y✝) z✝) = descFunLift F s (add x✝ (add y✝ z✝))
[PROOFSTEP]
dsimp
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s x✝ + descFunLift F s y✝ + descFunLift F s z✝ =
    descFunLift F s x✝ + (descFunLift F s y✝ + descFunLift F s z✝)
[PROOFSTEP]
rw [add_assoc]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : ↑(colimit F)
x✝¹ x✝ : Prequotient F
⊢ ZeroHom.toFun { toFun := descFun F s, map_zero' := (_ : descFun F s 0 = descFun F s 0) }
      (Quot.mk Setoid.r x✝¹ + Quot.mk Setoid.r x✝) =
    ZeroHom.toFun { toFun := descFun F s, map_zero' := (_ : descFun F s 0 = descFun F s 0) } (Quot.mk Setoid.r x✝¹) +
      ZeroHom.toFun { toFun := descFun F s, map_zero' := (_ : descFun F s 0 = descFun F s 0) } (Quot.mk Setoid.r x✝)
[PROOFSTEP]
dsimp [(· + ·)]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : ↑(colimit F)
x✝¹ x✝ : Prequotient F
⊢ descFun F s (Add.add (Quot.mk Setoid.r x✝¹) (Quot.mk Setoid.r x✝)) =
    Add.add (descFun F s (Quot.mk Setoid.r x✝¹)) (descFun F s (Quot.mk Setoid.r x✝))
[PROOFSTEP]
rw [← quot_add F]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : ↑(colimit F)
x✝¹ x✝ : Prequotient F
⊢ descFun F s (Quot.mk Setoid.r (add x✝¹ x✝)) =
    Add.add (descFun F s (Quot.mk Setoid.r x✝¹)) (descFun F s (Quot.mk Setoid.r x✝))
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
[PROOFSTEP]
change (m : ColimitType F →+ s.pt) _ = (descMorphism F s : ColimitType F →+ s.pt) _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x using Prequotient.recOn with
| of j x => exact FunLike.congr_fun (w j) x
| zero =>
  dsimp only [quot_zero]
  rw [map_zero, map_zero]
| neg x ih =>
  dsimp only [quot_neg]
  rw [map_neg, map_neg, ih]
| add x y ihx ihy =>
  simp only [quot_add]
  erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x using Prequotient.recOn with
| of j x => exact FunLike.congr_fun (w j) x
| zero =>
  dsimp only [quot_zero]
  rw [map_zero, map_zero]
| neg x ih =>
  dsimp only [quot_neg]
  rw [map_neg, map_neg, ih]
| add x y ihx ihy =>
  simp only [quot_add]
  erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]

| of j x => exact FunLike.congr_fun (w j) x
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]
exact FunLike.congr_fun (w j) x
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Quot Setoid.r
⊢ ↑m (Quot.mk Setoid.r zero) = ↑(descMorphism F s) (Quot.mk Setoid.r zero)
[PROOFSTEP]

| zero =>
  dsimp only [quot_zero]
  rw [map_zero, map_zero]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Quot Setoid.r
⊢ ↑m (Quot.mk Setoid.r zero) = ↑(descMorphism F s) (Quot.mk Setoid.r zero)
[PROOFSTEP]
dsimp only [quot_zero]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Quot Setoid.r
⊢ ↑m 0 = ↑(descMorphism F s) 0
[PROOFSTEP]
rw [map_zero, map_zero]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]

| neg x ih =>
  dsimp only [quot_neg]
  rw [map_neg, map_neg, ih]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]
dsimp only [quot_neg]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
⊢ ↑m (-Quot.mk Setoid.r x) = ↑(descMorphism F s) (-Quot.mk Setoid.r x)
[PROOFSTEP]
rw [map_neg, map_neg, ih]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x y : Prequotient F
ihx : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
ihy : ↑m (Quot.mk Setoid.r y) = ↑(descMorphism F s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑(descMorphism F s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]

| add x y ihx ihy =>
  simp only [quot_add]
  erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x y : Prequotient F
ihx : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
ihy : ↑m (Quot.mk Setoid.r y) = ↑(descMorphism F s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑(descMorphism F s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]
simp only [quot_add]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x y : Prequotient F
ihx : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
ihy : ↑m (Quot.mk Setoid.r y) = ↑(descMorphism F s) (Quot.mk Setoid.r y)
⊢ ↑m (Add.add (Quot.mk Setoid.r x) (Quot.mk Setoid.r y)) =
    ↑(descMorphism F s) (Add.add (Quot.mk Setoid.r x) (Quot.mk Setoid.r y))
[PROOFSTEP]
erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ f ≫ mk' (AddMonoidHom.range f) = 0
[PROOFSTEP]
ext x
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑(f ≫ mk' (AddMonoidHom.range f)) x = ↑0 x
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case w.a
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑f x ≈ 0
[PROOFSTEP]
apply leftRel_apply.mpr
[GOAL]
case w.a
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ -↑f x + 0 ∈ AddMonoidHom.range f
[PROOFSTEP]
fconstructor
[GOAL]
case w.a.w
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑G
case w.a.h G H : AddCommGroupCat f : G ⟶ H x : ↑G ⊢ ↑f ?w.a.w = -↑f x + 0
[PROOFSTEP]
exact -x
[GOAL]
case w.a.h
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑f (-x) = -↑f x + 0
[PROOFSTEP]
simp only [add_zero, AddMonoidHom.map_neg]
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑(cokernel.π f) (↑f x) = 0
[PROOFSTEP]
exact cokernel.condition_apply f x
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0) ≫
      lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) =
    𝟙 (cokernel f)
[PROOFSTEP]
refine coequalizer.hom_ext ?_
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ coequalizer.π f 0 ≫
      cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0) ≫
        lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)
[PROOFSTEP]
simp only [coequalizer_as_cokernel, cokernel.π_desc_assoc, Category.comp_id]
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ mk' (AddMonoidHom.range f) ≫
      lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) =
    cokernel.π f
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) ≫
      cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0) =
    𝟙 (of (↑H ⧸ AddMonoidHom.range f))
[PROOFSTEP]
ext x
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
x : ↑(of (↑H ⧸ AddMonoidHom.range f))
⊢ ↑(lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) ≫
          cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0))
      x =
    ↑(𝟙 (of (↑H ⧸ AddMonoidHom.range f))) x
[PROOFSTEP]
exact QuotientAddGroup.induction_on x <| cokernel.π_desc_apply f _ _
