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

State before:
n : ℕ
a b : FinInt n
⊢ toUint a ≡ toUint b [2^n] → a = b
Tactic:
intros h
State after:
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ a = b

State before:
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ a = b
Tactic:
apply eq_of_toUint_eq
State after:
case a
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ toUint a = toUint b

State before:
case a
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ toUint a = toUint b
Tactic:
apply cong2_to_eq n h toUint_bounds toUint_bounds
State after:
no goals