Fix build against Mathlib at Lean v4.29.1

[edu-ap]

Fixes the build against Mathlib at Lean v4.29.1. Two independent breakages, both small. Reported in #30.

1. Interval/Fixed.lean — Fixed.ofInt0_natCast

On current Mathlib, simp normalises both sides of the goal to the same term but no longer closes it, leaving a literal X = X. Appending rfl closes it.

2. Preinterval.mix' — a real-valued argument defeats erasure

mix' took a real-valued implicit argument whose only purpose was to state the proposition in the next argument:

def mix' (x : Preinterval) {a : ℝ} (m : approx x a) : Interval

A real is data, not a proof, so it is not erased. mix' is @[inline], and at its sole definitional call site — Interval.mul — that argument instantiates to a term containing Floating.val, which is noncomputable by design. Interval.mul therefore failed with "depends on Floating.val, which is noncomputable".

Moving the real inside the proposition means nothing real crosses the boundary:

def mix' (x : Preinterval) (m : ∃ a : ℝ, approx x a) : Interval

mix' has exactly one non-lemma use, so this touches one definition, two lemma signatures and one call site.

Testing

With these changes, Interval.Interval.Mul, Interval.Interval.Exp and Interval.Interval.Log all build against Mathlib v4.29.1 (rev 5e932f97).

Note that consumers also need to pin Mathlib's full transitive dependency closure explicitly, declared before interval, or Lake resolves batteries to main and Cli to v4.27.0-rc1 and overrides Mathlib's own pinned set. That is a packaging observation, not part of this PR.

Deliberately not addressed

Interval.Interval.Pow still fails via Interval/Interval/Division.lean. It is the same underlying problem in a harder place: there the real is a type index (Around x.val⁻¹), computed through Real.instInv, so this fix does not transfer. Repairing it needs a decision about whether Around should carry its centre as an index — a design question rather than a repair, and yours to make.

The lean-toolchain pin is deliberately left untouched.