mathlib

8a318021 - chore(category_theory/comma): removed obviously tactic for data fields (#18440)

chore(category_theory/comma): removed obviously tactic for data fields (#18440) For some `comma` categories like `structured_arrow`, `over`, `under`, the definition of some data fields could be obtained automatically by the obviously tactic. This PR removes this behaviour. Instead, specialized constructors like `structured_arrow.mk` or `structured_arrow.hom_mk` are used more systematically.