src/HOL/Library/Formal_Power_Series.thy

   apply (auto intro:  binomial_symmetric)
   done
 
 lemma Vandermonde_pochhammer_lemma:
   fixes a :: "'a::field_char_0"
-  assumes b: "\<forall> j\<in>{0 ..<n}. b \<noteq> of_nat j"
+  assumes b: "\<forall>j\<in>{0 ..<n}. b \<noteq> of_nat j"
   shows "setsum (\<lambda>k. (pochhammer (- a) k * pochhammer (- (of_nat n)) k) /
       (of_nat (fact k) * pochhammer (b - of_nat n + 1) k)) {0..n} =
     pochhammer (- (a + b)) n / pochhammer (- b) n"
   (is "?l = ?r")
 proof -

       with b show False using j by auto
     qed
 
     from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0"
       by (rule pochhammer_neq_0_mono)
-    {
-      assume k0: "k = 0 \<or> n =0"
-      then have "b gchoose (n - k) =
-        (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
-        using kn
-        by (cases "k = 0") (simp_all add: gbinomial_pochhammer)
-    }
-    moreover
-    {
-      assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0"
+
+    consider "k = 0 \<or> n = 0" | "n \<noteq> 0" "k \<noteq> 0" by blast
+    then have "b gchoose (n - k) =
+      (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
+    proof cases
+      case 1
+      then show ?thesis
+        using kn by (cases "k = 0") (simp_all add: gbinomial_pochhammer)
+    next
+      case 2
       then obtain m where m: "n = Suc m"
         by (cases n) auto
-      from k0 obtain h where h: "k = Suc h"
+      from \<open>k \<noteq> 0\<close> obtain h where h: "k = Suc h"
         by (cases k) auto
-      have "b gchoose (n - k) =
-        (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
+      show ?thesis
       proof (cases "k = n")
         case True
         then show ?thesis
           using pochhammer_minus'[where k=k and b=b]
           apply (simp add: pochhammer_same)

         also have "\<dots> = b gchoose (n - k)"
           unfolding th1 th2
           using kn' by (simp add: gbinomial_def)
         finally show ?thesis by simp
       qed
-    }
-    ultimately have "b gchoose (n - k) =
+    qed
+    then have "b gchoose (n - k) =
         (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
       "pochhammer (1 + b - of_nat n) k \<noteq> 0 "
       apply (cases "n = 0")
       using nz'
       apply auto
-      apply (cases k)
-      apply auto
       done
   }
   note th00 = this
-  have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
+  have "?r = ((a + b) gchoose n) * (of_nat (fact n) / (?m1 n * pochhammer (- b) n))"
     unfolding gbinomial_pochhammer
     using bn0 by (auto simp add: field_simps)
   also have "\<dots> = ?l"
     unfolding gbinomial_Vandermonde[symmetric]
     apply (simp add: th00)