Commit 2026-05-19 21:21 1fb6b288

View on Github →

chore: use to_fun to auto-generate more duplicate lemmas (#34279) We use the new functionality of to_fun from #34257 to remove a few more duplicate lemmas.

Estimated changes

deleted theorem Finset.analyticAt_fun_sum
deleted theorem Finset.analyticOn_fun_sum
deleted theorem HasDerivAt.fun_pow
deleted theorem derivWithin_fun_pow
deleted theorem deriv_fun_pow
deleted theorem Differentiable.fun_pow
deleted theorem DifferentiableAt.fun_pow
deleted theorem DifferentiableOn.fun_pow
deleted theorem HasFDerivAt.fun_pow'
deleted theorem fderivWithin_fun_pow'
deleted theorem fderivWithin_fun_pow
deleted theorem fderiv_fun_pow'
deleted theorem fderiv_fun_pow
deleted theorem iteratedDeriv_fun_add
deleted theorem iteratedDeriv_fun_id
deleted theorem iteratedDeriv_fun_mul
deleted theorem iteratedDeriv_fun_neg
deleted theorem iteratedDeriv_fun_sub