no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.755506
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
i : γ → β
hf : Summable f
hi : Injective i
⊢ Summable (f ∘ i)
simpa only [Set.indicator_range_comp] using
  (hi.summable_iff (fun x hx => Set.indicator_of_not_mem hx _)).2 (hf.indicator (Set.range i))