English
mkAux is the auxiliary inductive construction that, given n, returns a short complex structure built from X₃, d₂, and a relation, continuing recursively.
Русский
mkAux — это вспомогательная индуктивная конструкция, которая, получив n, возвращает структуру ShortComplex, построенную из X₃, d₂ и связи, продолжающуюся рекурсивно.
LaTeX
$$$\\mathrm{mkAux}: \\mathbb{N} \\to \\text{ShortComplex } V$, with\\ mkAux(0) = ShortComplex.mk _ _ s and mkAux(n+1) = ShortComplex.mk _ _ (succ (mkAux n)).2.2$$
Lean4
@[simp]
theorem mk'_d_1_0 : (mk' X₀ X₁ d₀ succ').d 1 0 = d₀ :=
by
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
rw [if_pos rfl, Category.id_comp]
/- Porting note:
Downstream constructions using `mk'` (e.g. in `CategoryTheory.Abelian.Projective`)
have very slow proofs, because of bad simp lemmas.
It would be better to write good lemmas here if possible, such as
```
theorem mk'_X_succ (j : ℕ) :
(mk' X₀ X₁ d₀ succ').X (j + 2) = (succ' ⟨_, _, (mk' X₀ X₁ d₀ succ').d (j + 1) j⟩).1 := by
sorry
theorem mk'_d_succ {i j : ℕ} :
(mk' X₀ X₁ d₀ succ').d (j + 2) (j + 1) =
eqToHom (mk'_X_succ X₀ X₁ d₀ succ' j) ≫
(succ' ⟨_, _, (mk' X₀ X₁ d₀ succ').d (j + 1) j⟩).2.1 :=
sorry
```
These are already tricky, and it may be better to write analogous lemmas for `mk` first.
-/
