Map of Yukawa Terms NSum to Finset

lemma map_ofYukawaTermsNSum_toFinset {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} {n : ℕ}:    ((map f x).ofYukawaTermsNSum n).toFinset = (x.ofYukawaTermsNSum n).toFinset.image f:= by  induction n with  | zero => simp [ofYukawaTermsNSum]  | succ n ih =>    simp [ofYukawaTermsNSum]    rw [Finset.image_union]    congr 1    ext i    simp only [Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map, Finset.mem_image,      exists_exists_and_exists_and_eq_and, map_add]    constructor    · intro h      obtain ⟨a, a_mem, b, b_mem, h⟩ := h      have a_mem' : a ∈ ((map f x).ofYukawaTermsNSum n).toFinset := by simpa using a_mem      rw [ih] at a_mem'      rw [mem_map_ofYukawaTerms_iff] at b_mem      simp at a_mem' b_mem      obtain ⟨a, a_mem', rfl⟩ := a_mem'      obtain ⟨b, b_mem', rfl⟩ := b_mem      exact ⟨a, a_mem', b, b_mem', h⟩    · intro h      obtain ⟨a, a_mem, b, b_mem, h⟩ := h      use f a      apply And.intro      · rw [← Multiset.mem_toFinset, ih]        simp only [Finset.mem_image, Multiset.mem_toFinset]        use a      use f b      apply And.intro      · rw [mem_map_ofYukawaTerms_iff]        simp only [Multiset.mem_map]        use b      exact h