lean-auto failure on simple model.

I have a trivial Lean spec:

import Auto
import Std.Data.BitVec
set_option auto.smt true
set_option auto.smt.trust true
set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true

inductive Zone where
  | Z1 | Z2 | Z3 | Z4
  -- Ask Lean to automatically show that type is not empty, has a representation function, and
  -- equality is decidable
  deriving Inhabited, Repr, DecidableEq

abbrev Area : Type := Int

def Zone.MinArea1 : Zone → Area
  | .Z1    => 10000
  | .Z2    => 5000
  | .Z3     => 3500
  | .Z4     => 2500

example (x: Zone) : x.MinArea1 >= 2500 := by cases x <;> simp -- succeeds
example (x: Zone) : x.MinArea1 >= 2500 := by cases x <;> auto -- fails

I can't seem to prove it by auto because it is not expanding the definition of MinArea1:

[auto.smt.printCommands] (declare-sort |Empty| 0) 

[auto.smt.printCommands] (define-fun |nsub| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|>=| |x| |y|) (|-| |x| |y|) 0)) 

[auto.smt.printCommands] (define-fun |itdiv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|div| |x| |y|) (|-| (|div| (|-| |x|) |y|))))) 

[auto.smt.printCommands] (define-fun |itmod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|mod| |x| |y|) (|-| (|mod| (|-| |x|) |y|))))) 

[auto.smt.printCommands] (define-fun |iediv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) 0 (|div| |x| |y|))) 

[auto.smt.printCommands] (define-fun |iemod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|mod| |x| |y|))) 

[auto.smt.printCommands] (declare-datatypes ((smti_0 0)) (((|smti_1|) (|smti_2|) (|smti_3|) (|smti_4|)))) 

[auto.smt.printCommands] (declare-fun |smti_5| (|smti_0|) |Int|) 

[auto.smt.printCommands] (assert (! (|not| (|<=| 2500 (|smti_5| |smti_1|))) :named valid_fact_0)) 

[auto.smt.result] z3 says Sat, model:
    ((|define-fun| |valid_fact_0| () |Bool| (|not| (|<=| 2500 (|smti_5| |smti_1|)))) (|define-fun| |smti_5| ((|x!0| |smti_0|)) |Int| 0))
    stderr:

I have tried a couple of things like asking lean-auto to unfold Zone.MinArea1: auto u[Zone.MinArea1] but this leads to an error: lamTerm2STerm :: Unexpected head term Auto.Embedding.Lam.LamTerm.lam (.atom 1) (.app (.base (.nat)) (.base (.icst (.iofNat))) (.base (.ncst (.natVal 10000))))

Can you tell me how to complete this proof properly? Also, is it possible to get lean-auto to handle the cases part?

Start by reproducing the minimal Zone, Zone.MinArea1, and auto examples in the issue, including the auto u[Zone.MinArea1] attempt. Trace how auto handles the cases goal and unfolds Zone.MinArea1; done means the reported proof succeeds or the limitation and supported workaround are documented.