src/HOL/Big_Operators.thy

   assumes fin: "finite A" "finite B"
   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
 proof -
   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
-    by(auto intro: finite_imageI)
+    by auto
   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
 qed