mathlib

9ee02c6c - feat(data/pfun): Remove unneeded assumption from pfun.fix_induction (#12920)

feat(data/pfun): Remove unneeded assumption from pfun.fix_induction (#12920) Removed a hypothesis from `pfun.fix_induction`. Note that it was two "layers" deep, so this is actually a strengthening. The original can be recovered by ```lean /-- A recursion principle for `pfun.fix`. -/ @[elab_as_eliminator] def fix_induction_original {f : α →. β ⊕ α} {b : β} {C : α → Sort*} {a : α} (h : b ∈ f.fix a) (H : ∀ a', b ∈ f.fix a' → (∀ a'', /- this hypothesis was removed -/ b ∈ f.fix a'' → sum.inr a'' ∈ f a' → C a'') → C a') : C a := by { apply fix_induction h, intros, apply H; tauto, } ``` Note that `eval_induction` copies this syntax, so the same argument was removed there as well. This allows for some simplifications of other parts of the code. Unfortunately, it was hard to figure out what was going on in the very dense parts of `tm_to_partrec.lean` and `partrec.lean`. I mostly just mechanically removed the hypotheses that were unnecessarily being supplied, and then checked if that caused some variable to be unused and removed that etc. But I cannot tell if this allows for greater simplifications. I also extracted two lemmas `fix_fwd` and `fix_stop` that I thought would be useful on their own.