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

State before:
n : ℕ
a : ℤ
⊢ a ≥ 0 ∧ a < 2 ^ n → mod2 a n = a
Tactic:
intros h
State after:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ mod2 a n = a

State before:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ mod2 a n = a
Tactic:
simp [mod2]
State after:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ a % 2 ^ n = a

State before:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ a % 2 ^ n = a
Tactic:
simp [Int.mod_bounds _ h.1 h.2]
State after:
no goals