Theorem: FinInt.add_toUint (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = mod2 (toUint n + toUint m) sz
Tactic:
rw [add_toUint_rem]
State after:
sz : ℕ
n m : FinInt sz
⊢ (if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz) =
    mod2 (toUint n + toUint m) sz

State before:
sz : ℕ
n m : FinInt sz
⊢ (if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz) =
    mod2 (toUint n + toUint m) sz
Tactic:
split
State after:
case inl
sz : ℕ
n m : FinInt sz
h✝ : toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m = mod2 (toUint n + toUint m) sz

case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz

State before:
case inl
sz : ℕ
n m : FinInt sz
h✝ : toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m = mod2 (toUint n + toUint m) sz

case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz
Tactic:
. simp [mod2_idem ⟨Int.add_ge_zero _ _ toUint_ge toUint_ge, by assumption⟩]
State after:
case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz

State before:
case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz
Tactic:
. sorry_arith
State after:
no goals

State before:
sz : ℕ
n m : FinInt sz
h✝ : toUint n + toUint m < 2 ^ sz
⊢ toUint ?m.152087 + toUint ?m.152089 < 2 ^ ?m.152070
Tactic:
assumption
State after:
no goals