mathlib

657df433 - refactor(linear_algebra/tensor_product): make `lift f (x ⊗ₜ y) = f x y` true by `rfl` (#18121)

refactor(linear_algebra/tensor_product): make `lift f (x ⊗ₜ y) = f x y` true by `rfl` (#18121) Since this is essentially the "primitive" recursor, it is very convenient for it to expand definitionally. With this change, the following lemmas are now rfl: * `algebra.mul'_apply` * `free_monoid.lift_comp_of` * `free_monoid.lift_eval_of` * `tensor_product.lie_module.lift_apply` * `alternating_map.dom_coprod'_apply` * `contract_left_apply` * `contract_right_apply` * `dual_tensor_hom_apply` * `derivation.tensor_product_to_tmul` * `poly_equiv_tensor.to_fun_linear_tmul_apply` * `tensor_product.lift.tmul` * `tensor_product.lift.tmul'` * `algebra.tensor_product.lift_tmul` * `algebra.tensor_product.lmul'_apply_tmul` * `tensor_product.algebra.smul_def` And one lemma is no longer rfl * `free_monoid.lift_apply`