leanprover-community/NNG4

Missing generalizing tactic in AdvMul

Closed this issue · 1 comments

ndren commented

image
I had to complete it with warnings/relaxed rules.

abentkamp commented

This had been fixed on the dev branch of lean4game already.