mathlib3

8aa26b27 - feat(tactic/linear_combination): improve error messages and degenerate case (#12062)

feat(tactic/linear_combination): improve error messages and degenerate case (#12062) This threads the expected type of the combination from the target throughout the tactic call. If no hypotheses are given to combine, the behavior is effectively to just call the normalization tactic. closes #11990 Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>