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

State before:
x y : ℤ
n : ℕ
⊢ x = y → mod2 x n = mod2 y n
Tactic:
intros h
State after:
x y : ℤ
n : ℕ
h : x = y
⊢ mod2 x n = mod2 y n

State before:
x y : ℤ
n : ℕ
h : x = y
⊢ mod2 x n = mod2 y n
Tactic:
simp [h]
State after:
no goals