Mathlib evaluationLeftAdjoint: rw/simp on Sigma.ι fail; change to explicit Sigma terms or use the unit

Terms like ((evaluationLeftAdjoint C j).obj X).map f have type L.obj t ⟶ L.obj t', which equals ∐ fun _ : j ⟶ t => X only at default transparency. Goals then print as Sigma.ι _ a ≫ Sigma.desc _ ≫ ... but rw [Sigma.ι_comp_desc_assoc] and simp silently fail ('not type-correct under implicit transparency'). Two fixes: (1) begin with change IsSplitMono (Sigma.desc fun g : j ⟶ t ↦ Sigma.ι (fun _ : j ⟶ t' ↦ X) (g ≫ f)), after which simp works; (2) in adjunction arguments, replace Sigma.ι _ (𝟙 j) by (evaluationAdjunctionRight C j).unit.app X and go through Adjunction.homEquiv_unit with fully explicit arguments, then exact (assoc _ _ _).trans key. Related: Mathlib has no HasFiniteBiproducts (J ⥤ C) instance; get it from HasFiniteBiproducts.of_hasFiniteProducts. Also, Projective (⨁ g) and Projective (∐ g) need the index type in the Hom universe, so for ⨁ j : J in a functor category you have to prove projectivity of the biproduct by hand (3 lines with choose + biproduct.desc).