src/HOL/Library/Binomial.thy

 lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
 proof-
   {assume kn: "k > n" 
     from kn binomial_eq_0[OF kn] have ?thesis 
       by (simp add: gbinomial_pochhammer field_simps
-	pochhammer_of_nat_eq_0_iff)}
+        pochhammer_of_nat_eq_0_iff)}
   moreover
   {assume "k=0" then have ?thesis by simp}
   moreover
   {assume kn: "k \<le> n" and k0: "k\<noteq> 0"
     from k0 obtain h where h: "k = Suc h" by (cases k, auto)

     have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" 
 "{1..n - Suc h} \<inter> {n - h .. n} = {}" and eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" using h kn by auto
     from eq[symmetric]
     have ?thesis using kn
       apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
-	gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
+        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
       apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
       unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
       unfolding mult_assoc[symmetric] 
       unfolding setprod_timesf[symmetric]
       apply simp