Lean4
/-- Auxiliary definition for `truncGE'.homologyData`. -/
noncomputable def isLimitKernelFork :
IsLimit (KernelFork.ofι _ (homologyι_truncGE'XIsoOpcycles_inv_d K e j k hj' hj)) :=
by
have hk' : c'.next j' = e.f k := by simpa only [hj'] using e.next_f hk
by_cases hjk : c.Rel j k
· let e : parallelPair ((K.truncGE' e).d j k) 0 ≅ parallelPair (K.fromOpcycles j' (e.f k)) 0 :=
parallelPair.ext (K.truncGE'XIsoOpcycles e hj' hj) (K.truncGE'XIso e rfl (e.not_boundaryGE_next hjk))
(by simp [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj]) (by simp)
exact
(IsLimit.postcomposeHomEquiv e _).1
(IsLimit.ofIsoLimit (K.homologyIsKernel _ _ hk') (Fork.ext (Iso.refl _) (by simp [e, Fork.ι])))
· have := K.isIso_homologyι _ _ hk' (shape _ _ _ (by simpa only [← hj', e.rel_iff] using hjk))
exact
IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (shape _ _ _ hjk))
(Fork.ext ((truncGE'XIsoOpcycles K e hj' hj) ≪≫ (asIso (K.homologyι j')).symm))
