Commit 2025-04-27 14:08 a569d485

feat: pull Function.update through recursors (#24318) This adds a quite technical lemma that can be used to generalize some existing lemmas for Sum The general version would in principle work for any enumerative inductive type, though only after currying the constructor arguments first. These are simp (in the direction pulling update to the outside) since that seemed to be useful for #18534, though I could see it either way.