PR #17142: fix(tactic/polyrith): fix crash when hypothese...

Stream: triage

[Random Issue Bot]

Today I chose PR 17142 for discussion!

fix(tactic/polyrith): fix crash when hypotheses are constant polynomials
Created by @Eric Wieser (@eric-wieser) on 2022-10-25
Labels: bug, t-meta

Is this PR still relevant? Any recent updates? Anyone making progress?

[Eric Wieser]

This probably needs forward-porting to mathlib4, I suspect no one will ever have time to review the mathlib3 version

[Kevin Buzzard]

@Rob Lewis do you have any comments on this?