mathlib4
mathlib4 copied to clipboard
feat: propagate_tags tactic
Adds propagate_tags
@Beanway144, sorry this languished on the PR queue for a while. Would you be able to merge the conflict and adopt Mario's suggestions?