Commit 2023-01-25 11:55 3041403b

View on Github →

fix: instantiate mvars before pattern matching on Type (#1775) As reported on Zulip.

Estimated changes

Modified Mathlib/Tactic/Linarith/Frontend.lean

added def Linarith.ExprMultiMap.find

added def Linarith.ExprMultiMap.insert

modified def Linarith.partitionByType

Modified Mathlib/Tactic/Linarith/Verification.lean

Modified test/linarith.lean