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

State before:
a b : ℤ
n : ℕ
⊢ a ≡ b [2^n] → a ≥ 0 ∧ a < 2 ^ n → b ≥ 0 ∧ b < 2 ^ n → a = b
Tactic:
intros h ha hb
State after:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ a = b

State before:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ a = b
Tactic:
rw [←mod2_idem ha, ←mod2_idem hb]
State after:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ mod2 a n = mod2 b n

State before:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ mod2 a n = mod2 b n
Tactic:
assumption
State after:
no goals