English
A higher-step version of the inductive auxiliary construction, parametrized by (i, j) with i+1 = j, giving a relation between the components of mkInductiveAux₂ at i and j.
Русский
Расширенная ступень конструкции, зависящая от пары индексов (i, j) с условием i+1 = j, устанавливающая связь между компонентами mkInductiveAux₂ на i и j.
LaTeX
$$$\forall i,j \in \mathbb{N},\ i+1=j \ all
(mkInductiveAux₂\ e\ zero\ comm_zero\ one\ comm_one\ succ\ i).2.1 \; ≫ \; (Q.xPrevIso\ h).hom = (P.xNextIso\ h).inv \; ≫ \\ (mkInductiveAux₂\ e\ zero\ comm_zero\ one\ comm_one\ succ\ j).1$$$
Lean4
@[simp]
theorem mkInductiveAux₂_zero :
mkInductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, zero ≫ (Q.xPrevIso rfl).inv, by simpa using comm_zero⟩ :=
rfl
