Lean4
/-- The function from the colimit ring to the cone point of any other cocone. -/
def descFun (s : Cocone F) : ColimitType F → s.pt :=
by
fapply Quot.lift
· exact descFunLift F s
· intro x y r
induction r with
| refl => rfl
| symm x y _ ih => exact ih.symm
| trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
| map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
| zero j => simp
| one j => simp
| neg j x => simp
| add j x y => simp
| mul j x y => simp
| neg_1 x x' r ih => dsimp; rw [ih]
| add_1 x x' y r ih => dsimp; rw [ih]
| add_2 x y y' r ih => dsimp; rw [ih]
| mul_1 x x' y r ih => dsimp; rw [ih]
| mul_2 x y y' r ih => dsimp; rw [ih]
| zero_add x => dsimp; rw [zero_add]
| add_zero x => dsimp; rw [add_zero]
| one_mul x => dsimp; rw [one_mul]
| mul_one x => dsimp; rw [mul_one]
| neg_add_cancel x => dsimp; rw [neg_add_cancel]
| add_comm x y => dsimp; rw [add_comm]
| add_assoc x y z => dsimp; rw [add_assoc]
| mul_assoc x y z => dsimp; rw [mul_assoc]
| left_distrib x y z => dsimp; rw [mul_add]
| right_distrib x y z => dsimp; rw [add_mul]
| zero_mul x => dsimp; rw [zero_mul]
| mul_zero x => dsimp; rw [mul_zero]
