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

State before:
a : ℤ
n : ℕ
⊢ smod2 a n < 2 ^ n
Tactic:
simp [smod2]
State after:
a : ℤ
n : ℕ
⊢ (if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)) < 2 ^ n

State before:
a : ℤ
n : ℕ
⊢ (if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)) < 2 ^ n
Tactic:
split
State after:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) - 2 ^ (n + 1) < 2 ^ n

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n

State before:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) - 2 ^ (n + 1) < 2 ^ n

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n
Tactic:
. sorry_arith
State after:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n

State before:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n
Tactic:
. sorry_arith
State after:
no goals