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

State before:
n : ℕ
⊢ mod2 (2 ^ n) n = 0
Tactic:
simp [mod2]
State after:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0

State before:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0
Tactic:
simp [Int.emod_self]
State after:
no goals