mathlib

41398242 - refactor(category_theory/differential_object): simp only -> simp_rw (#13333)

refactor(category_theory/differential_object): simp only -> simp_rw (#13333) This is extremely minor; I replace a `simp only` with a `simp_rw`. This proof is apparently rather fragile with respect to some other changes I'm trying to make, and I worked out the correct `simp_rw` sequence while debugging. May as well preserve it for posterity, or at least until next time I make it break. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>