Data.Pfun Issues Summary ( mathlib4#1179)

Stream: mathlib4

[Arien Malec]

For mathlib4#1179, the current issues are:

1) Bug in generalize_proofs in fix_induction_spec (same issue as https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Extracting.20a.20proof.20from.20a.20dependent.20function.20call/near/321740648 -- I was able to use the revert/intro trick in one place but not here
2) tactic bug in prodMap_comp_comp (See: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.22.28kernel.29.20declaration.20has.20metavariables.22/near/322790931)
3) Generally complicated motive state for mem_fix_iff and a couple of other issues (see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/my.20PRs.20that.20need.20help/near/322639477) -- I can't follow @Kevin Buzzard's suggestion on making fix computable because WellFounded.fixF is noncomputable but perhaps there's a definition that doesn't refer to WellFounded.fixF

[Arien Malec]

Actually the noncomputable annotation seems to be a red herring -- mem_fix_iff doesn't depend on anything noncomputable...