mathlib3

7bebee66 - chore(category_theory/monad/equiv_mon): Removing some slow uses of `obviously` (#11980)

chore(category_theory/monad/equiv_mon): Removing some slow uses of `obviously` (#11980) Providing explicit proofs for various fields rather than leaving them for `obviously` (and hence `tidy`) to fill in. Follow-up to this suggestion by Kevin Buzzard in [this Zulip comment](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60tidy.60.20in.20mathlib.20proofs/near/271474418). (These are temporary changes until `obviously` can be tweaked to do this more quickly)