summable_of_le_on_nonzero

lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀ i ≠ 0, g i ≤ f i)    (summablef : Summable f) : Summable g := by  set f' : ℤ → ℝ := fun i ↦ if i = 0 then g i else f i with f'def  have : ∀ i, g i ≤ f' i := by    intro i    rw [f'def]    by_cases h : i = 0    · simp [h]    · simp only [h]; exact hgf i h  apply Summable.of_nonneg_of_le hgpos this  let s : Finset ℤ := {0}  rw [← s.summable_compl_iff]  refine (summable_congr fun ⟨b, hb⟩ ↦ ?_).mpr (s.summable_compl_iff.mpr summablef)  rw [mem_singleton] at hb  exact if_neg hb