chore(CategoryTheory/HomologicalComplex): make ChainComplex.of implicit reducible

[Thmoas-Guan]

This PR makes ChainComplex.of implicit reducible def instaed of previous abbrev.
We also removed the auxiliary definition ChainComplex.of.d, for unification of simp lemmas for applictions of ChainComplex.of, since d is no longer simping to ChainComplex.of.d.

Co-authored-by: @Whysoserioushah

---

[github-actions]

PR summary e96e3c6faf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ obj_d'
+ of_d'
- of.d

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e96e3c6).

• +3 new declarations
• −4 removed declarations

+AlgebraicTopology.NormalizedMooreComplex.obj_d'
-ChainComplex.of.d
-ChainComplex.of.d.congr_simp
+ChainComplex.of_d'
+groupHomology.chainsFunctor_obj
-groupHomology.chainsFunctor_obj_X_carrier
-groupHomology.chainsFunctor_obj_d

---

Decrease in strong tech debt: (relative, absolute) = (2.58, 0.00)

Current number	Change	Type (strong)
backward.defeqAttrib.useBackward	4224	-4
backward.isDefEq.respectTransparency	4678	-1

No changes to weak technical debt.

Current commit e96e3c6faf
Reference commit 98b840bb29

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Thmoas-Guan]

!bench

[leanprover-radar]

Benchmark results for fa72d0d against 98b840b are in. No significant results found. @Thmoas-Guan

• 🟥 build//instructions: +12.8G (+0.01%)

Small changes (1✅, 6🟥)

• 🟥 build/module/Mathlib.AlgebraicTopology.AlternatingFaceMapComplex//instructions: +782.4M (+4.80%)
• 🟥 build/module/Mathlib.AlgebraicTopology.MooreComplex//instructions: +620.0M (+6.51%)
• 🟥 build/module/Mathlib.AlgebraicTopology.SimplicialSet.Homology.Relative//instructions: +686.1M (+3.46%)
• 🟥 build/module/Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro//instructions: +1.3G (+10.24%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality//instructions: -2.0G (-1.48%)
• 🟥 build/module/Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence//instructions: +2.3G (+12.19%) (reduced significance based on *//lines)
• 🟥 build/module/Mathlib.RepresentationTheory.Homological.TateCohomology.Basic//instructions: +678.7M (+2.88%)

[Thmoas-Guan]

!bench

[leanprover-radar]

Benchmark results for e96e3c6 against 98b840b are in. No significant results found. @Thmoas-Guan

• 🟥 build//instructions: +46.0G (+0.03%)

Small changes (8🟥)

• 🟥 build/module/Batteries.Lean.Meta.Inaccessible//instructions: +26.8M (+1.86%)
• 🟥 build/module/Mathlib.AlgebraicTopology.AlternatingFaceMapComplex//instructions: +818.7M (+5.02%)
• 🟥 build/module/Mathlib.AlgebraicTopology.MooreComplex//instructions: +631.4M (+6.63%)
• 🟥 build/module/Mathlib.AlgebraicTopology.SimplicialSet.Homology.Relative//instructions: +684.7M (+3.46%)
• 🟥 build/module/Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro//instructions: +1.3G (+10.12%)
• 🟥 build/module/Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence//instructions: +2.1G (+11.35%) (reduced significance based on *//lines)
• 🟥 build/module/Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree//instructions: +1.9G (+1.75%)
• 🟥 build/module/Mathlib.RepresentationTheory.Homological.TateCohomology.Basic//instructions: +935.1M (+3.97%)

[joelriou]

Then, you may remove the of_X lemma below (which is not doing exactly the same thing, but I do not think it matters):

Suggested change

	@[implicit_reducible]
	@[implicit_reducible, simps X]

[joelriou]

I think of_d should be a simp lemma, but not of_d'. Following the simps X suggestion above, I think it would make sense to replace this with

@[simp]
theorem of_d (j : α) : dsimp% (of X d sq).d (j + 1) j = d j := by

[joelriou]

It would probably be a good idea to do the same for CochainComplex.of in the same PR.