isLimit — Mathlib

Lean4
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms,
then the kernel of `φ f g : X ⊞ Y ⟶ Y ⊞ Z` identifies
to `kernel (f ≫ g)`. -/
noncomputable def isLimit : IsLimit (KernelFork.ofι _ (ι_φ f g)) :=
  KernelFork.IsLimit.ofι' _ _
    (fun {A} k hk ↦ by
      refine ⟨kernel.lift _ (k ≫ biprod.fst) ?_, ?_⟩
      all_goals
        obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_to k
        simp only [biprod.ext_to_iff, add_comp, assoc, inl_φ, BinaryBicone.inl_fst, comp_id, inr_φ_fst, comp_neg,
          zero_comp, BinaryBicone.inl_snd, comp_zero, φ_snd, BinaryBicone.inr_snd_assoc, zero_add,
          add_neg_eq_zero] at hk
        obtain ⟨rfl, hk⟩ := hk
        aesop)
Похожие утверждения