fix: prove the mkAppRangeAux equation instead of assuming it

[kim-em]

This PR replaces the Expr.mkAppRangeAux.eq_def axiom in Lean4Lean/Verify/Axioms.lean with a proved theorem. The axiom was a workaround for leanprover/lean4#8464; that has since merged, so mkAppRangeAux is a total definition in the pinned toolchain and its defining equation follows from rw [mkAppRangeAux]. The statement is unchanged, so the consumer in Lean4Lean/Verify/Expr.lean needs no edits, and no replacement assumptions are introduced: #print axioms Lean.Expr.mkAppRangeAux.eq_def reports only propext and Quot.sound.

Closes #25

🤖 Prepared with Claude Code

[digama0]

🤖 Pushed a commit on top — I think we can drop the declaration entirely rather than prove it.

lean4#8464 having merged does more than make the equation provable: it makes mkAppRangeAux a total definition, so Lean generates mkAppRangeAux.eq_def on demand. Verify/Expr.lean already opens the private mkAppRangeAux at line 628, so the rw [mkAppRangeAux.eq_def] at its only use site picks up the generated lemma with no edit at all. The generated statement is character-for-character the one being removed:

mkAppRangeAux.eq_def : ∀ (n : Nat) (args : Array Expr) (i : Nat) (e : Expr),
  mkAppRangeAux n args i e = if i < n then mkAppRangeAux n args (i + 1) (mkApp e args[i]!) else e

So keeping our own copy shadows the generated lemma and leaves us maintaining a restatement of a definition we don't own — it would silently drift if the upstream definition ever changed shape, and the rw would keep working against our stale copy.

Same axiom result you reported, with nothing left behind:

#print axioms Lean.Expr.mkAppRange_eq   ->   [propext, Quot.sound]

lake build is clean (143 jobs, 23 sorrys, unchanged), and Verify/Axioms.lean goes from 8 axioms to 7 — the remaining ones are the genuinely unprovable PersistentHashMap/PersistentArray ones where the upstream definitions are opaque.