Theorem: IMOSL.IMO2012A5.𝔽₂X.toList_inj (IMOSLLean4/Extra/F2X/toList.lean)

State before:
P Q : 𝔽₂X
h : P.toList = Q.toList
⊢ P.toFinset = Q.toFinset
Tactic:
rw [← 𝔽₂X.toFinset_toList, h, 𝔽₂X.toFinset_toList]
State after:
no goals