bad heuristic in leanchecker

[bryangingechen]

leanprover-community/mathlib#3185 exposed a bug in leanchecker.

See zulip thread.

[digama0]

Here is a small test:

class A := (a b : ℕ)
def T : A := {a := 1, b := 10000}
def U : A := {a := 1, b := 100 * 100}
def foo : @A.a T = @A.a U := rfl

lean -E test.txt --only-export=foo test.lean
leanchecker mathlib.txt