`simp`, `omega` in `module` cause type mismatch in kernel

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

A call to simp followed by omega in a module leads to an "application type mismatch" error in the kernel. The problem seems to be related to Int8.reduceToInt.

Steps to Reproduce

Run this:

module

-- import all Init.Data.SInt.Basic -- solves the problem

/--
error: (kernel) application type mismatch
  Eq.trans
    (congrArg (fun x => (Int8.ofInt x).toInt)
      (congr (congrArg (fun x => HAdd.hAdd ↑x) (UInt8.toNat_add x 1)) (Int8.toInt_neg 128)))
    Int8.toInt_ofInt
argument has type
  (Int8.ofInt (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8))).toInt =
    (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8)).bmod Int8.size
but function has type
  (Int8.ofInt (↑((x.toNat + UInt8.toNat 1) % 2 ^ 8) + (-Int8.toInt 128).bmod (2 ^ 8))).toInt =
      (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8)).bmod Int8.size →
    (Int8.ofInt (↑(x + 1).toNat + (-128).toInt)).toInt =
      (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8)).bmod Int8.size
-/
#guard_msgs in
example {x : UInt8}
    (h : (Int8.ofInt (↑(x + 1).toNat + Int8.minValue.toInt)).toInt = Int8.minValue.toInt) :
    256 ∣ ↑x.toNat + 1 := by
  -- squashed form of: simp [Int.natCast_emod, Int.bmod_eq_iff] at h ⊢
  -- reducing `Int8.reduceToInt` solves the problem
  simp only [UInt8.toNat_add, UInt8.reduceToNat, Int.natCast_emod, Int.cast_ofNat_Int, Int8.toInt_neg,
    Int8.reduceToInt, Int8.toInt_ofInt, Nat.zero_lt_succ, Int.bmod_eq_iff] at h ⊢
  omega

Expected behavior:

Either omega or simp themselves fail, or they succeed and generate a proof term the kernel is happy with.

Actual behavior:

simp and omega together create a proof term that does not type check in the kernel.

(Note that omega does not see anything related to Int8, so that omega itself does not really seem to be the problem. However, the error also goes away if omega is replaced with sorry.)

Versions

Lean 4.25.0-nightly-2025-09-24
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproducer from the issue against Lean 4.25.0-nightly-2025-09-24, focusing on the interaction between simp, omega, and Int8.reduceToInt. Trace the generated proof term around the reported Eq.trans mismatch; done means the reproducer is rejected by a tactic or its resulting proof is accepted by the kernel.