∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ}, HasSum (fun a => MulOpposite.unop (f a)) (MulOpposite.unop a) L = HasSum f a L