mathlib

ce72cde8 - feat(category_theory/limits): special shapes API cleanup (#2423)

feat(category_theory/limits): special shapes API cleanup (#2423) This is the 2.5th PR in a series of most likely three PRs about the cohomology functor. This PR has nothing to do with cohomology, but I'm going to need a lemma from this pull request in the final PR in the series. In this PR, I * perform various documentation and cleanup tasks * add lemmas similar to the ones seen in #2396 for equalizers, kernels and pullbacks (NB: these are not needed for biproducts since the `simp` and `ext` lemmas for products and coproducts readily fire) * generalize `prod.hom_ext` to the situation where we have a `binary_fan X Y` and an `is_limit` for that specific fan (and similar for the other shapes) * add "bundled" versions of lift and desc. Here is the most important example: ```lean def kernel.lift' {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : {l : W ⟶ kernel f // l ≫ kernel.ι f = k} := ⟨kernel.lift f k h, kernel.lift_ι _ _ _⟩ ``` This definition doesn't really do anything by itself, but it makes proofs comforable and readable. For example, if you say `obtain ⟨t, ht⟩ := kernel.lift' g p hpg`, then the interesting property of `t` is right there in the tactic view, which I find helpful in keeping track of things when a proof invokes a lot of universal properties.