sumResiduesIn_inter_eq_of_set_eq

lemma sumResiduesIn_inter_eq_of_set_eq {F : ℂ → ℂ} {Rn S2 P : Set ℂ}    (h_set_eq : Rn ∩ P = S2 ∩ P)    (h_residue_zero : ∀ s ∈ S2, s ∉ P → residue F s = 0) :    sumResiduesIn F (Rn ∩ P) = sumResiduesIn F S2 := by  rw [sumResiduesIn, sumResiduesIn, tsum_subtype, tsum_subtype]  apply tsum_congr  intro s  by_cases hs_S2 : s ∈ S2  · by_cases hs_pole : s ∈ P    · have hs_rect_pole : s ∈ Rn ∩ P := h_set_eq.symm ▸ ⟨hs_S2, hs_pole⟩      simp [hs_S2, hs_rect_pole]    · have hs_not_rect_pole : s ∉ Rn ∩ P := fun hs => hs_pole hs.2      have hres0 : residue F s = 0 := h_residue_zero s hs_S2 hs_pole      simp [hs_S2, hs_not_rect_pole, hres0]  · have hs_not_rect_pole : s ∉ Rn ∩ P := fun hs => hs_S2 (h_set_eq ▸ hs).1    simp [hs_S2, hs_not_rect_pole]