Mem mem finset of no Exotics

lemma mem_mem_finset_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (hnZ : F.HasNoZero)    (x : Fluxes) (hx : x ∈ F) :    x ∈ ({⟨1, -1⟩, ⟨1, 0⟩, ⟨1, 1⟩, ⟨2, -1⟩, ⟨2, 0⟩, ⟨2, 1⟩, ⟨3, 0⟩} : Finset Fluxes) := by  rcases x with f  simp only [Int.reduceNeg, Finset.mem_insert, Finset.mem_singleton]  have hQ1 := F.mem_chiralIndicesOfQ_mem_of_noExotics hF x.M (Multiset.mem_map.mpr ⟨x, hx, rfl⟩)  have hU1 := F.mem_chiralIndicesOfU_mem_of_noExotics hF (x.M - x.N)    (Multiset.mem_map.mpr ⟨x, hx, rfl⟩)  have hE1 := F.mem_chiralIndicesOfE_mem_of_noExotics hF (x.M + x.N)    (Multiset.mem_map.mpr ⟨x, hx, rfl⟩)  have h0 : ¬ x = 0 := by    by_contra hn    subst hn    exact hnZ hx  rcases x with ⟨M, N⟩  let D := M + N  have hd : N = D - M := by omega  generalize D = D' at *  subst hd  simp only [add_sub_cancel] at hE1  simp_all only [Int.reduceNeg, Fluxes.mk.injEq]  clear hx D  revert h0 hU1  revert D'  revert M  decide