Preimage Of Finset eq

lemma preimageOfFinset_eq (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩1) :    preimageOfFinset S5 S10 f x = {y : ChargeSpectrum 𝓩 | y.map f = x ∧ y ∈ ofFinset S5 S10} := by  ext y  simp [preimageOfFinset, toProd]  match y, x with  | ⟨yHd, yHu, y5, y10⟩, ⟨xHd, xHu, x5, x10⟩ =>  simp [map]  constructor  · intro ⟨⟨h1, rfl⟩, ⟨h2, rfl⟩, ⟨h3, rfl⟩, ⟨h4, rfl⟩⟩    simp only [true_and]    rw [mem_ofFinset_iff]    simp only    refine ⟨?_, ?_, ?_, ?_⟩    · match yHd with      | some a => simpa using h1      | none => simp    · match yHu with      | some a => simpa using h2      | none => simp    · exact h3.trans <| Finset.filter_subset (fun y => f y ∈ Finset.image (⇑f) y5) S5    · apply h4.trans <| Finset.filter_subset (fun y => f y ∈ Finset.image (⇑f) y10) S10  · intro ⟨⟨rfl, rfl, rfl, rfl⟩, h2⟩    simp only [and_true, Finset.mem_image]    rw [mem_ofFinset_iff] at h2    simp at h2    refine ⟨?_, ?_, ?_, ?_⟩    · match yHd with      | some a =>        simp at h2        simpa using h2.1      | none => simp    · match yHu with      | some a =>        simp at h2        simpa using h2.2.1      | none => simp    · refine Finset.subset_iff.mpr ?_      intro x hx      simp only [Finset.mem_filter]      refine ⟨h2.2.2.1 hx, ?_⟩      use x    · refine Finset.subset_iff.mpr ?_      intro x hx      simp only [Finset.mem_filter]      refine ⟨h2.2.2.2 hx, ?_⟩      use x