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

State before:
sz : ℕ
n : ℤ
⊢ toUint (ofInt sz n) = mod2 n sz
Tactic:
induction sz
State after:
case zero
n : ℤ
⊢ toUint (ofInt Nat.zero n) = mod2 n Nat.zero

case succ
n : ℤ
n✝ : ℕ
n_ih✝ : toUint (ofInt n✝ n) = mod2 n n✝
⊢ toUint (ofInt (Nat.succ n✝) n) = mod2 n (Nat.succ n✝)

State before:
n : ℤ
⊢ toUint (ofInt Nat.zero n) = mod2 n Nat.zero
Tactic:
case zero =>
  simp [mod2]; sorry_arith
State after:
no goals

State before:
n : ℤ
sz : ℕ
ih : toUint (ofInt sz n) = mod2 n sz
⊢ toUint (ofInt (Nat.succ sz) n) = mod2 n (Nat.succ sz)
Tactic:
case succ sz ih =>
  sorry
State after:
no goals

State before:
n : ℤ
⊢ toUint (ofInt Nat.zero n) = mod2 n Nat.zero
Tactic:
simp [mod2]
State after:
n : ℤ
⊢ 0 = n % 1

State before:
n : ℤ
⊢ 0 = n % 1
Tactic:
sorry_arith
State after:
no goals

State before:
n : ℤ
sz : ℕ
ih : toUint (ofInt sz n) = mod2 n sz
⊢ toUint (ofInt (Nat.succ sz) n) = mod2 n (Nat.succ sz)
Tactic:
sorry
State after:
no goals