English
A base case for the auxiliary second inductive construction: at index 0, mkCoinductiveAux₂ yields a simple pair with the initial isomorphism and the given zero map.
Русский
База для второй вспомогательной индуктивной конструкции: при индексе 0 mkCoinductiveAux₂ даёт простую пару с начальным изоморфизмом и данным нулевым отображением.
LaTeX
$$mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, (P.xNextIso rfl).hom ≫ zero, by simpa using comm_zero⟩$$
Lean4
theorem mkCoinductiveAux₃ (i j : ℕ) (h : i + 1 = j) :
(P.xNextIso h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).2.1 =
(mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).1 ≫ (Q.xPrevIso h).hom :=
by
subst j
rcases i with (_ | _ | i) <;> simp [mkCoinductiveAux₂]
