mathlib3

f9bac45c - chore(category_theory/linear/yoneda): Removing some slow uses of `obviously` (#11979)

chore(category_theory/linear/yoneda): Removing some slow uses of `obviously` (#11979) Providing explicit proofs for `map_id'` and `map_comp'` rather than leaving them for `obviously` (and hence `tidy`) to fill in. Suggested by Kevin Buzzard in [this Zulip comment](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60tidy.60.20in.20mathlib.20proofs/near/271474418). Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> (These are temporary changes until `obviously` can be tweaked to do this more quickly)