Apply eq sum even term Of Mass Dim

lemma apply_eq_sum_even_termOfMassDim {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)    (hV : IsInvariant V) (φ : HiggsVec) :    V φ = ∑ m ∈ Finset.range (n / 2 + 1), termOfMassDim V h (2 * m) φ := by  rw [apply_eq_sum_termOfMassDim h, ← Finset.sum_filter_add_sum_filter_not    (Finset.range (n + 1)) Even]  have hodd : ∑ m ∈ (Finset.range (n + 1)).filter (fun m => ¬ Even m),      termOfMassDim V h m φ = 0 := by    refine Finset.sum_eq_zero fun m hm => ?_    simp only [Finset.mem_filter] at hm    exact termOfMassDim_zero_of_odd h m hV φ (Nat.not_even_iff_odd.mp hm.2)  rw [hodd, add_zero]  have hset : (Finset.range (n / 2 + 1)).image (fun k => 2 * k)      = (Finset.range (n + 1)).filter Even := by    ext a    simp only [Finset.mem_image, Finset.mem_range, Finset.mem_filter, Nat.even_iff]    constructor    · rintro ⟨k, hk, rfl⟩      omega    · rintro ⟨ha, hae⟩      exact ⟨a / 2, by omega, by omega⟩  rw [← hset, Finset.sum_image fun x _ y _ hxy => by omega]