English
A simple additive lemma expressing how mkInductiveAux₂ behaves under increment of the degree, expressing the new index (n+1) in terms of the previous auxiliary I = mkInductiveAux₁ e … n.
Русский
Простая лемма аддитивности, описывающая, как mkInductiveAux₂ ведёт себя при увеличении степени на единицу, выражая новый индекс через предшествующий вспомогательный объект I = mkInductiveAux₁ e … n.
LaTeX
$$$mkInductiveAux₂\ e\ zero\ comm_zero\ one\ comm_one\ succ\ (n+1) = \\text{let } I := mkInductiveAux₁\ e\ zero\ one\ comm_one\ succ\ n\ in \\langle (P.xNextIso\ rfl).hom \circ I.1, I.2.1 \circ (Q.xPrevIso\ rfl).inv, \text{I.2.2} \rangle$$$
Lean4
@[simp]
theorem mkInductiveAux₂_add_one (n) :
mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
letI I := mkInductiveAux₁ e zero one comm_one succ n
⟨(P.xNextIso rfl).hom ≫ I.1, I.2.1 ≫ (Q.xPrevIso rfl).inv, by simpa using I.2.2⟩ :=
rfl
