src/HOL/Groups_Big.thy

   show ?thesis
     unfolding F_eq using fin nn eq
     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
 qed
 
-lemma delta:
+lemma delta [simp]:
   assumes fS: "finite S"
   shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
 proof -
   let ?f = "(\<lambda>k. if k = a then b k else \<^bold>1)"
   show ?thesis

       using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
     with True show ?thesis by simp
   qed
 qed
 
-lemma delta':
+lemma delta' [simp]:
   assumes fin: "finite S"
   shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   using delta [OF fin, of a b, symmetric] by (auto intro: cong)
 
 lemma If_cases: