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

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

State before:
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ a = b
Tactic:
rw [←smod2_idem ha, ←smod2_idem hb]
State after:
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ smod2 a n = smod2 b n

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