mathlib3

ca7dca39 - feat(geometry/manifold/algebra/smooth_functions): simp lemmas for coercions to functions (#6893)

feat(geometry/manifold/algebra/smooth_functions): simp lemmas for coercions to functions (#6893) These came up while working on the branch `replace_algebra_def` but seem worth adding in their own right.