diff --git a/thys/Interpolation_Polynomials_HOL_Algebra/Bounded_Degree_Polynomials.thy b/thys/Interpolation_Polynomials_HOL_Algebra/Bounded_Degree_Polynomials.thy
--- a/thys/Interpolation_Polynomials_HOL_Algebra/Bounded_Degree_Polynomials.thy
+++ b/thys/Interpolation_Polynomials_HOL_Algebra/Bounded_Degree_Polynomials.thy
@@ -1,171 +1,160 @@
 section \<open>Bounded Degree Polynomials\<close>
 
 text \<open>This section contains a definition for the set of polynomials with a degree bound and
 establishes its cardinality.\<close>
 
 theory Bounded_Degree_Polynomials
   imports "HOL-Algebra.Polynomial_Divisibility"
 begin
 
 lemma (in ring) coeff_in_carrier: "p \<in> carrier (poly_ring R) \<Longrightarrow> coeff p i \<in> carrier R"
-  using poly_coeff_in_carrier carrier_is_subring  by (simp add: univ_poly_carrier)
+  using poly_coeff_in_carrier carrier_is_subring by (simp add: univ_poly_carrier)
 
 definition bounded_degree_polynomials
   where "bounded_degree_polynomials F n = {x. x \<in> carrier (poly_ring F) \<and> (degree x < n \<or> x = [])}"
 
 text \<open>Note: The definition for @{term "bounded_degree_polynomials"} includes the zero polynomial
 in @{term "bounded_degree_polynomials F 0"}. The reason for this adjustment is that, contrary to
-definition in HOL Algebra, most authors set the degree of the zero polynomial to 
+definition in HOL Algebra, most authors set the degree of the zero polynomial to
 $-\infty$~\cite[\textsection 7.2.2]{shoup2009computational}. That
 definition make some identities, such as $\mathrm{deg}(f g) = \mathrm{deg}\, f + \mathrm{deg}\, g$
 for polynomials $f$ and $g$ unconditionally true.
-In particular, it prevents an unnecessary corner case in the statement of the results established 
+In particular, it prevents an unnecessary corner case in the statement of the results established
 in this entry.\<close>
 
 lemma bounded_degree_polynomials_length:
   "bounded_degree_polynomials F n = {x. x \<in> carrier (poly_ring F) \<and> length x \<le> n}"
-  apply (simp add:bounded_degree_polynomials_def)
-  apply (rule Collect_cong)
-  by (metis Suc_pred length_greater_0_conv less_Suc_eq_0_disj less_Suc_eq_le linorder_not_le)
+  unfolding bounded_degree_polynomials_def using leI order_less_le_trans by fastforce
 
 lemma (in ring) fin_degree_bounded:
   assumes "finite (carrier R)"
   shows "finite (bounded_degree_polynomials R n)"
 proof -
   have "bounded_degree_polynomials R n \<subseteq> {p. set p \<subseteq> carrier R \<and> length p \<le> n}"
-    apply (rule subsetI)
-    apply (simp add: bounded_degree_polynomials_length) using assms(1) 
-    by (meson polynomial_incl univ_poly_carrier)
-  thus ?thesis  apply (rule finite_subset)
-    using assms(1) finite_lists_length_le by auto
+    unfolding bounded_degree_polynomials_length
+    using assms polynomial_incl univ_poly_carrier by blast
+  thus ?thesis
+    using assms finite_lists_length_le finite_subset by fast
 qed
 
 lemma (in ring) non_empty_bounded_degree_polynomials:
   "bounded_degree_polynomials R k \<noteq> {}"
 proof -
   have "\<zero>\<^bsub>poly_ring R\<^esub> \<in> bounded_degree_polynomials R k"
     by (simp add: bounded_degree_polynomials_def univ_poly_zero univ_poly_zero_closed)
   thus ?thesis by auto
 qed
 
 lemma in_image_by_witness:
   assumes "\<And>x. x \<in> A \<Longrightarrow> g x \<in> B \<and> f (g x) = x"
   shows "A \<subseteq> f ` B"
   by (metis assms image_eqI subsetI)
 
 lemma card_mostly_constant_maps:
   assumes "y \<in> B"
-  shows "card {f. range f \<subseteq> B \<and> (\<forall>x. x \<ge> n \<longrightarrow> f x = y)} = card B ^ n" (is "card ?A = ?B") 
+  shows "card {f. range f \<subseteq> B \<and> (\<forall>x. x \<ge> n \<longrightarrow> f x = y)} = card B ^ n" (is "card ?A = ?B")
 proof -
   define f where "f = (\<lambda>f k. if k < n then f k else y)"
 
+  have a:"?A \<subseteq> (f ` ({0..<n}  \<rightarrow>\<^sub>E B))"
+    unfolding f_def
+    by (rule in_image_by_witness[where g="\<lambda>f. restrict f {0..<n}"], auto)
+
+  have b:"(f ` ({0..<n}  \<rightarrow>\<^sub>E B)) \<subseteq> ?A"
+    using f_def assms by auto
+
+  have c: "inj_on f ({0..<n} \<rightarrow>\<^sub>E B)"
+    by (rule inj_onI, metis PiE_E atLeastLessThan_iff ext f_def)
+
   have "card ?A = card (f ` ({0..<n}  \<rightarrow>\<^sub>E B))"
-    apply (rule arg_cong[where f="card"])
-    apply (rule order_antisym) (* TODO Split *)
-     apply (rule in_image_by_witness[where g="\<lambda>f. restrict f {0..<n}"])
-     apply (rule conjI, simp add: range_subsetD)
-     apply (rule ext, simp add:restrict_def Pi_def PiE_def f_def)
-    apply (rule image_subsetI, simp add:f_def)
-    apply (rule conjI) 
-     apply (metis Int_iff PiE PiE_def atLeastLessThan_iff image_Collect_subsetI less_eq_nat.simps(1))
-    by (rule image_subsetI, rule assms)
+    using a b by auto
   also have "... = card ({0..<n} \<rightarrow>\<^sub>E B)"
-    apply (rule card_image, rule inj_onI, rule ext, simp add:f_def)
-    by (metis PiE_arb atLeastLessThan_iff)
+    by (metis c card_image)
   also have "... = card B ^ n"
-    by (subst card_PiE, simp, simp)
+    by (simp add: card_PiE[OF finite_atLeastLessThan])
   finally show ?thesis by simp
 qed
 
 definition (in ring) build_poly where
   "build_poly f n = normalize (rev (map f [0..<n]))"
 
 lemma (in ring) poly_degree_bound_from_coeff:
   assumes "x \<in> carrier (poly_ring R)"
   assumes "\<And>k. k \<ge> n \<Longrightarrow> coeff x k = \<zero>"
   shows "degree x < n \<or> x = \<zero>\<^bsub>poly_ring R\<^esub>"
 proof (rule ccontr)
   assume a:"\<not>(degree x < n \<or> x = \<zero>\<^bsub>poly_ring R\<^esub>)"
-  hence b:"lead_coeff x \<noteq> \<zero>\<^bsub>R\<^esub>" 
+  hence b:"lead_coeff x \<noteq> \<zero>\<^bsub>R\<^esub>"
     by (metis assms(1) polynomial_def univ_poly_carrier univ_poly_zero)
-  hence "coeff x (degree x) \<noteq> \<zero>" 
+  hence "coeff x (degree x) \<noteq> \<zero>"
     by (metis a lead_coeff_simp univ_poly_zero)
   moreover have "degree x \<ge> n" by (meson a not_le)
   ultimately show "False" using assms(2) by blast
-qed          
+qed
 
 lemma (in ring) poly_degree_bound_from_coeff_1:
   assumes "x \<in> carrier (poly_ring R)"
   assumes "\<And>k. k \<ge> n \<Longrightarrow> coeff x k = \<zero>"
   shows "x \<in> bounded_degree_polynomials R n"
   using poly_degree_bound_from_coeff[OF assms]
   by (simp add:bounded_degree_polynomials_def univ_poly_zero assms)
 
-lemma (in ring)
-  assumes "\<And>i. i < n \<Longrightarrow> f i \<in> carrier R"
-  shows 
-    build_poly_poly: "build_poly f n \<in> carrier (poly_ring R)" and
-    build_poly_coeff: "\<And>i. coeff (build_poly f n) i = (if i < n then f i else \<zero>)" and
-    build_poly_degree: "degree (build_poly f n) \<le> n - 1"
-proof -
-  show a:"build_poly f n \<in> carrier (poly_ring R)"
-    apply (simp add:build_poly_def univ_poly_carrier[symmetric])
-    apply (rule normalize_gives_polynomial, simp)
-    using assms atLeastLessThan_iff by blast
+lemma (in ring) length_build_poly:
+  "length (build_poly f n) \<le> n"
+  by (metis length_map build_poly_def normalize_length_le length_rev length_upt
+      less_imp_diff_less linorder_not_less)
 
-  show b:"\<And>i. coeff (build_poly f n) i = (if i < n then f i else \<zero>)"
-  proof -
-    fix i :: nat
-    show "coeff (build_poly f n) i = (if i < n then f i else \<zero>)"
-      apply (cases "i < n")
-      apply (simp add:build_poly_def normalize_coeff[symmetric])
-       apply (subst coeff_nth, simp, simp add:rev_nth)
-      apply (simp add:build_poly_def normalize_coeff[symmetric])
-      by (subst coeff_length, simp, simp)
-  qed
+lemma (in ring) build_poly_degree:
+  "degree (build_poly f n) \<le> n-1"
+  using length_build_poly diff_le_mono by presburger
 
-  have "degree (build_poly f n) < n \<or> build_poly f n = \<zero>\<^bsub>poly_ring R\<^esub>"
-    apply (rule poly_degree_bound_from_coeff[OF a])
-    using b by simp
+lemma (in ring) build_poly_poly:
+  assumes "\<And>i. i < n \<Longrightarrow> f i \<in> carrier R"
+  shows "build_poly f n \<in> carrier (poly_ring R)"
+  unfolding build_poly_def univ_poly_carrier[symmetric]
+  by (rule normalize_gives_polynomial, simp add:image_subset_iff Ball_def assms)
 
-  thus "degree (build_poly f n) \<le> n - 1"
-    apply (cases n, simp add:build_poly_def)
-    by (metis diff_Suc_1 diff_is_0_eq less_Suc_eq_le list.size(3) univ_poly_zero zero_diff)
+lemma (in ring) build_poly_coeff:
+  "coeff (build_poly f n) i = (if i < n then f i else \<zero>)"
+proof -
+  show "coeff (build_poly f n) i = (if i < n then f i else \<zero>)"
+    unfolding build_poly_def normalize_coeff[symmetric]
+    by (cases "i < n", (simp add:coeff_nth rev_nth coeff_length)+)
 qed
 
-lemma (in ring) length_build_poly: 
-  "length (build_poly f n) \<le> n"
-  apply (simp add:build_poly_def)
-  by (metis length_map normalize_length_le length_rev length_upt less_imp_diff_less linorder_not_less)
+lemma (in ring) build_poly_bounded:
+  assumes "\<And>k. k < n \<Longrightarrow> f k \<in> carrier R"
+  shows "build_poly f n \<in> bounded_degree_polynomials R n"
+  unfolding bounded_degree_polynomials_length
+  using build_poly_poly[OF assms] length_build_poly by auto
 
 text \<open>The following establishes the total number of polynomials with a degree less than $n$.
-Unlike the results in the following sections, it is already possible to establish this property for 
+Unlike the results in the following sections, it is already possible to establish this property for
 polynomials with coefficients in a ring.\<close>
 
 lemma (in ring) bounded_degree_polynomials_card:
   "card (bounded_degree_polynomials R n) = card (carrier R) ^ n"
 proof -
   have a:"coeff ` bounded_degree_polynomials R n \<subseteq> {f. range f \<subseteq> (carrier R) \<and> (\<forall>k \<ge> n. f k = \<zero>)}"
-    apply (rule image_subsetI, simp add:bounded_degree_polynomials_def, rule conjI) 
-    using coeff_length coeff_in_carrier by auto
+    by (rule image_subsetI, auto simp add:bounded_degree_polynomials_def coeff_length coeff_in_carrier)
 
   have b:"{f. range f \<subseteq> (carrier R) \<and> (\<forall>k \<ge> n. f k = \<zero>)} \<subseteq> coeff ` bounded_degree_polynomials R n"
     apply (rule in_image_by_witness[where g="\<lambda>x. build_poly x n"])
-    apply (rule conjI, rule poly_degree_bound_from_coeff_1)
-      apply (rule build_poly_poly, blast) 
-     apply (subst coeff_length, metis length_build_poly order_trans, simp)
-    by (rule ext, subst build_poly_coeff, blast, simp)
+    by (auto simp add:build_poly_coeff intro:build_poly_bounded)
+
+  have "inj_on coeff (carrier (poly_ring R))"
+    by (rule inj_onI, simp add: coeff_iff_polynomial_cond univ_poly_carrier)
+
+  hence coeff_inj: "inj_on coeff (bounded_degree_polynomials R n)"
+    using inj_on_subset bounded_degree_polynomials_def by blast
 
   have "card ( bounded_degree_polynomials R n) = card (coeff `  bounded_degree_polynomials R n)"
-    apply (rule card_image[symmetric])
-    apply (rule inj_on_subset[where A="carrier (poly_ring R)"])
-     apply (rule inj_onI, simp add: coeff_iff_polynomial_cond univ_poly_carrier)
-    by (simp add:bounded_degree_polynomials_def)
+    using coeff_inj card_image[symmetric] by blast
   also have "... = card {f. range f \<subseteq> (carrier R) \<and> (\<forall>k \<ge> n. f k = \<zero>)}"
     by (rule arg_cong[where f="card"], rule order_antisym[OF a b])
-  also have "... = card (carrier R)^n" 
+  also have "... = card (carrier R)^n"
     by (rule card_mostly_constant_maps, simp)
   finally show ?thesis by simp
 qed
 
 end
\ No newline at end of file
diff --git a/thys/Interpolation_Polynomials_HOL_Algebra/Interpolation_Polynomial_Cardinalities.thy b/thys/Interpolation_Polynomials_HOL_Algebra/Interpolation_Polynomial_Cardinalities.thy
--- a/thys/Interpolation_Polynomials_HOL_Algebra/Interpolation_Polynomial_Cardinalities.thy
+++ b/thys/Interpolation_Polynomials_HOL_Algebra/Interpolation_Polynomial_Cardinalities.thy
@@ -1,394 +1,375 @@
 section \<open>Cardinalities of Interpolation Polynomials\<close>
 
-text \<open>This section establishes the cardinalities of the set of polynomials with a degree bound 
+text \<open>This section establishes the cardinalities of the set of polynomials with a degree bound
 interpolating a given set of points.\<close>
 
 theory Interpolation_Polynomial_Cardinalities
   imports Bounded_Degree_Polynomials Lagrange_Interpolation
 begin
 
 lemma (in ring) poly_add_coeff:
   assumes "x \<in> carrier (poly_ring R)"
   assumes "y \<in> carrier (poly_ring R)"
   shows "coeff (x \<oplus>\<^bsub>poly_ring R\<^esub> y) k = coeff x k \<oplus> coeff y k"
-  apply (subst univ_poly_add)
-  apply (subst poly_add_coeff)
-    apply (metis assms(1) univ_poly_carrier polynomial_incl)
-   apply (metis assms(2) univ_poly_carrier polynomial_incl)
-  by simp
+  by (metis assms univ_poly_carrier polynomial_incl univ_poly_add poly_add_coeff)
 
 lemma (in domain) poly_neg_coeff:
   assumes "x \<in> carrier (poly_ring R)"
   shows "coeff (\<ominus>\<^bsub>poly_ring R\<^esub> x) k = \<ominus>coeff x k"
 proof -
   interpret x:cring "poly_ring R"
-    using assms cring_def carrier_is_subring  domain.univ_poly_is_cring domain_axioms by auto
+    using assms cring_def carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
+
   have a:"\<zero>\<^bsub>poly_ring R\<^esub> = x \<ominus>\<^bsub>poly_ring R\<^esub> x"
-    using x.r_right_minus_eq assms(1) by metis
+    by (metis x.r_right_minus_eq assms(1))
+
   have "\<zero> = coeff (\<zero>\<^bsub>poly_ring R\<^esub>) k" by (simp add:univ_poly_zero)
-  also have "... = coeff x k \<oplus> coeff (\<ominus>\<^bsub>poly_ring R\<^esub> x) k" using a
-    apply (simp)
-    apply (subst a_minus_def, subst poly_add_coeff)
-      apply (metis assms)
-     using assms univ_poly_carrier polynomial_incl apply blast
-    by simp
+  also have "... = coeff x k \<oplus> coeff (\<ominus>\<^bsub>poly_ring R\<^esub> x) k" using a assms
+    by (simp add:a_minus_def poly_add_coeff)
   finally have "\<zero> = coeff x k \<oplus> coeff (\<ominus>\<^bsub>poly_ring R\<^esub> x) k" by simp
   thus ?thesis
-    by (metis local.minus_minus x.a_inv_closed sum_zero_eq_neg coeff_in_carrier assms) 
+    by (metis local.minus_minus x.a_inv_closed sum_zero_eq_neg coeff_in_carrier assms)
 qed
 
 lemma (in domain) poly_substract_coeff:
   assumes "x \<in> carrier (poly_ring R)"
   assumes "y \<in> carrier (poly_ring R)"
   shows "coeff (x \<ominus>\<^bsub>poly_ring R\<^esub> y) k = coeff x k \<ominus> coeff y k"
 proof -
   interpret x:cring "poly_ring R"
-    using assms cring_def carrier_is_subring  domain.univ_poly_is_cring domain_axioms by auto
+    using assms cring_def carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
   show ?thesis
-    apply (simp add:a_minus_def)
-      apply (subst poly_add_coeff[OF assms(1)])
-     apply (rule x.a_inv_closed[OF assms(2)])
-    apply (subst poly_neg_coeff[OF assms(2)])
-    by simp
+    using assms by (simp add:a_minus_def poly_add_coeff poly_neg_coeff)
 qed
 
 text \<open>A polynomial with more zeros than its degree is the zero polynomial.\<close>
 
 lemma (in field) max_roots:
   assumes "p \<in> carrier (poly_ring R)"
   assumes "K \<subseteq> carrier R"
   assumes "finite K"
   assumes "degree p < card K"
   assumes "\<And>x. x \<in> K \<Longrightarrow> eval p x = \<zero>"
   shows "p = \<zero>\<^bsub>poly_ring R\<^esub>"
 proof (rule ccontr)
   assume "p \<noteq> \<zero>\<^bsub>poly_ring R\<^esub>"
   hence a:"p \<noteq> []" by (simp add: univ_poly_zero)
   have "\<And>x. count (mset_set K) x \<le> count (roots p) x"
   proof -
     fix x
     show "count (mset_set K) x \<le> count (roots p) x"
     proof (cases "x \<in> K")
       case True
       hence "is_root p x"
-        by (meson a  assms(2) assms(5) is_ring is_root_def subsetD)
+        by (meson a assms(2,5) is_ring is_root_def subsetD)
       hence "x \<in> set_mset (roots p)"
         using assms(1) roots_mem_iff_is_root field_def by force
       hence "1 \<le> count (roots p) x" by simp
       moreover have "count (mset_set K) x = 1" using True assms(3) by simp
       ultimately show ?thesis by presburger
     next
       case False
       hence "count (mset_set K) x = 0" by simp
       then show ?thesis by presburger
     qed
   qed
   hence "mset_set K \<subseteq># roots p"
     by (simp add: subseteq_mset_def)
-  hence "card K \<le> size (roots p)" 
+  hence "card K \<le> size (roots p)"
     by (metis size_mset_mono size_mset_set)
   moreover have "size (roots p) \<le> degree p"
     using a size_roots_le_degree assms by auto
   ultimately show "False" using assms(4)
     by (meson leD less_le_trans)
 qed
 
 definition (in ring) split_poly
   where "split_poly K p = (restrict (eval p) K, \<lambda>k. coeff p (k+card K))"
 
-text \<open>To establish the count of the number of polynomials of degree less than 
-$n$ interpolating a function $f$ on $K$ where $\lvert K \rvert \leq n$, the function 
-@{term "split_poly K"} establishes a bijection between the polynomials of degree less than 
+text \<open>To establish the count of the number of polynomials of degree less than
+$n$ interpolating a function $f$ on $K$ where $\lvert K \rvert \leq n$, the function
+@{term "split_poly K"} establishes a bijection between the polynomials of degree less than
 $n$ and the values of the polynomials on $K$ in combination with the coefficients of order
 $\lvert K \rvert$ and greater.
 
 For the injectivity: Note that the difference of two polynomials whose coefficients of order
-$\lvert K \rvert$ and larger agree must have a degree less than $\lvert K \rvert$ and because 
-their values agree on $k$ points, it must have $\lvert K \rvert$ zeros and hence is the zero 
+$\lvert K \rvert$ and larger agree must have a degree less than $\lvert K \rvert$ and because
+their values agree on $k$ points, it must have $\lvert K \rvert$ zeros and hence is the zero
 polynomial.
 
-For the surjectivty: Let $p$ be a polynomial whose coefficients larger than $\lvert K \rvert$ are 
+For the surjectivty: Let $p$ be a polynomial whose coefficients larger than $\lvert K \rvert$ are
 chosen, and all other coefficients be $0$. Now it is possible to find a polynomial $q$ interpolating
 $f - p$ on $K$ using Lagrange interpolation. Then $p + q$ will interpolate $f$ on $K$ and because
 the degree of $q$ is less than $\lvert K \rvert$ its coefficients of order $\lvert K \rvert$ will
 be the same as those of $p$.
 
 A tempting question is whether it would be easier to instead establish a bijection between the
 polynomials of degree less than $n$ and its values on $K \cup K'$ where $K'$ are arbitrarily chosen
-$n-\lvert K \rvert$ points in the field. This approach is indeed easier, however, it fails for 
+$n-\lvert K \rvert$ points in the field. This approach is indeed easier, however, it fails for
 the case where the size of the field is less than $n$.\<close>
 
 lemma (in field) split_poly_inj:
   assumes "finite K"
   assumes "K \<subseteq> carrier R"
   shows "inj_on (split_poly K) (carrier (poly_ring R))"
 proof
   fix x
   fix y
   assume a1:"x \<in> carrier (poly_ring R)"
   assume a2:"y \<in> carrier (poly_ring R)"
   assume a3:"split_poly K x = split_poly K y"
 
   interpret x:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
 
   have x_y_carrier: "x \<ominus>\<^bsub>poly_ring R\<^esub> y \<in> carrier (poly_ring R)" using a1 a2 by simp
   have "\<And>k. coeff x (k+card K) = coeff y (k+card K)"
-    using a3 apply (simp add:split_poly_def) by meson
-  hence b:"\<And>k. coeff (x \<ominus>\<^bsub>poly_ring R\<^esub> y) (k+card K) = \<zero>"
+    using a3 by (simp add:split_poly_def, meson)
+  hence "\<And>k. coeff (x \<ominus>\<^bsub>poly_ring R\<^esub> y) (k+card K) = \<zero>"
     using coeff_in_carrier a1 a2 by (simp add:poly_substract_coeff)
-  have "degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) < card K \<or> (x \<ominus>\<^bsub>poly_ring R\<^esub> y) = \<zero>\<^bsub>poly_ring R\<^esub>"
-    apply (rule poly_degree_bound_from_coeff, rule x.minus_closed[OF a1 a2])
-    by (metis add.commute le_iff_add b)
+  hence "degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) < card K \<or> (x \<ominus>\<^bsub>poly_ring R\<^esub> y) = \<zero>\<^bsub>poly_ring R\<^esub>"
+    by (metis poly_degree_bound_from_coeff add.commute le_iff_add x_y_carrier)
   moreover have "\<And>k. k \<in> K \<Longrightarrow> eval x k = eval y k"
-    using a3 apply (simp add:split_poly_def restrict_def) by meson 
+    using a3 by (simp add:split_poly_def restrict_def, meson)
   hence "\<And>k. k \<in> K \<Longrightarrow> eval x k \<ominus> eval y k = \<zero>"
-    using eval_in_carrier univ_poly_carrier polynomial_incl a1 a2 
-    by (metis assms(2) in_mono r_right_minus_eq) 
+    by (metis eval_in_carrier univ_poly_carrier polynomial_incl a1 assms(2) in_mono r_right_minus_eq)
   hence "\<And>k. k \<in> K \<Longrightarrow> eval (x \<ominus>\<^bsub>poly_ring R\<^esub> y) k = \<zero>"
-    apply (subst ring_hom_cring.hom_sub[OF eval_cring_hom[OF carrier_is_subring]])
-    using assms(2) a1 a2 by auto
+    using a1 a2 subsetD[OF assms(2)] carrier_is_subring
+    by (simp add: ring_hom_cring.hom_sub[OF eval_cring_hom])
   ultimately have "x \<ominus>\<^bsub>poly_ring R\<^esub> y = \<zero>\<^bsub>poly_ring R\<^esub>"
     using max_roots x_y_carrier assms by blast
   then show "x = y"
     using x.r_right_minus_eq[OF a1 a2] by simp
 qed
 
 lemma (in field) split_poly_image:
   assumes "finite K"
   assumes "K \<subseteq> carrier R"
   shows "split_poly K ` carrier (poly_ring R) \<supseteq>
-        (K \<rightarrow>\<^sub>E carrier R) \<times> {f. range f \<subseteq> carrier R \<and> (\<exists>n. \<forall>k \<ge> n. f k = \<zero>\<^bsub>R\<^esub>)}" 
+        (K \<rightarrow>\<^sub>E carrier R) \<times> {f. range f \<subseteq> carrier R \<and> (\<exists>n. \<forall>k \<ge> n. f k = \<zero>\<^bsub>R\<^esub>)}"
 proof (rule subsetI)
   fix x
-  assume e:"x \<in> (K \<rightarrow>\<^sub>E carrier R) \<times> {f. range f \<subseteq> carrier R \<and> (\<exists>(n::nat). \<forall>k \<ge> n. f k = \<zero>)}"
-  have a1: "fst x \<in> (K \<rightarrow>\<^sub>E carrier R)" 
-    using e by (simp add:mem_Times_iff)
+  assume a:"x \<in> (K \<rightarrow>\<^sub>E carrier R) \<times> {f. range f \<subseteq> carrier R \<and> (\<exists>(n::nat). \<forall>k \<ge> n. f k = \<zero>)}"
+  have a1: "fst x \<in> (K \<rightarrow>\<^sub>E carrier R)"
+    using a by (simp add:mem_Times_iff)
   obtain n where a2: "snd x \<in> {f. range f \<subseteq> carrier R \<and> (\<forall>k \<ge> n. f k = \<zero>)}"
-    using e mem_Times_iff by force
+    using a mem_Times_iff by force
+  have a3: "\<And>y. snd x y \<in> carrier R" using a2 by blast
 
   define w where "w = build_poly (\<lambda>i. if i \<ge> card K then (snd x (i - card K)) else \<zero>) (card K + n)"
 
   have w_carr: "w \<in> carrier (poly_ring R)"
-    apply (simp add:w_def)
-    apply (rule build_poly_poly, simp)
-    using a2 PiE_def by blast
+    unfolding w_def by (rule build_poly_poly, simp add:a3)
 
   have w_eval_range: "\<And>x. x \<in> carrier R \<Longrightarrow> local.eval w x \<in> carrier R"
   proof -
     fix x
     assume w_eval_range_1:"x \<in> carrier R"
     interpret x:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p x)"
-      apply (rule eval_cring_hom[OF carrier_is_subring]) using assms w_eval_range_1 by blast
+      using eval_cring_hom[OF carrier_is_subring] assms w_eval_range_1 by blast
     show "eval w x \<in> carrier R"
       by (rule x.hom_closed[OF w_carr])
   qed
 
   interpret r:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
 
   define y where "y = interpolate K (\<lambda>k. fst x k \<ominus> eval w k)"
   define r where "r = y \<oplus>\<^bsub>poly_ring R\<^esub> w"
 
-  have y_poly: "y \<in> carrier (poly_ring R)" 
-    apply (simp add:y_def, rule interpolate_poly[OF assms(1) assms(2)])
-    apply (rule image_subsetI)
-    apply (rule minus_closed) using a1 PiE_def Pi_def apply blast
-    by (metis w_eval_range subsetD[OF assms(2)])
+  have x_minus_w_in_carrier: "\<And>z. z \<in> K \<Longrightarrow> fst x z \<ominus> eval w z \<in> carrier R"
+    using a1 PiE_def Pi_def minus_closed subsetD[OF assms(2)] w_eval_range by auto
+
+  have y_poly: "y \<in> carrier (poly_ring R)" unfolding y_def
+    using x_minus_w_in_carrier interpolate_poly[OF assms(1) assms(2)] image_subsetI by force
 
   have y_degree: "degree y \<le> card K - 1"
-    apply (subst y_def, rule interpolate_degree[OF assms(1) assms(2)])
-    apply (rule image_subsetI, rule minus_closed) using a1 PiE_def Pi_def apply blast
-    by (metis w_eval_range subsetD[OF assms(2)])
+    unfolding y_def
+    using x_minus_w_in_carrier interpolate_degree[OF assms(1) assms(2)] image_subsetI by force
+
+  have y_len: "length y \<le> card K"
+  proof (cases "K={}")
+    case True
+    then show ?thesis
+      by (simp add:y_def interpolate_def univ_poly_zero)
+  next
+    case False
+    then show ?thesis
+      by (metis y_degree Suc_le_D assms(1) card_gt_0_iff diff_Suc_1 not_less_eq_eq order.strict_iff_not)
+  qed
 
   have r_poly: "r \<in> carrier (poly_ring R)"
-    apply (simp add:r_def)
-    using y_poly w_carr by simp
+    using r_def y_poly w_carr by simp
 
   have coeff_r: "\<And>k. coeff r (k + card K) = snd x k"
   proof -
     fix k :: nat
+    have y_len': "length y \<le> k + card K" using y_len trans_le_add2 by blast
     have "coeff r (k + card K) = coeff y (k + card K) \<oplus> coeff w (k+card K)"
       by (simp add:r_def  poly_add_coeff[OF y_poly w_carr])
     also have "... = \<zero> \<oplus> coeff w (k+card K)"
-      apply (cases "K = {}", simp add:y_def interpolate_def univ_poly_zero)
-      apply (subst coeff_length)
-       apply (metis One_nat_def assms(1) y_degree bot.extremum card.empty card_seteq le_add2 
-          le_diff_iff not_less_eq_eq order.trans zero_le)
-      by simp
+      using coeff_length[OF y_len'] by simp
     also have "... = coeff w (k+card K)"
       using coeff_in_carrier[OF w_carr] by simp
     also have "... = snd x k"
-      apply (simp add:w_def)
-      apply (subst build_poly_coeff, simp)
-      using a2 Pi_def apply blast
-      using a2 by (simp add:not_less)
+      using a2 by (simp add:w_def build_poly_coeff not_less)
     finally show "coeff r (k + card K) = snd x k" by simp
   qed
 
   have eval_r: "\<And>k. k \<in> K \<Longrightarrow> eval r k = fst x k"
   proof -
     fix k
-    assume d:"k \<in> K"
+    assume b:"k \<in> K"
     interpret s:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p k)"
-      apply (rule eval_cring_hom[OF carrier_is_subring]) using assms d by blast
+      using eval_cring_hom[OF carrier_is_subring] assms b by blast
 
-    have k_carr: "k \<in> carrier R" using assms(2) d by blast
-    have fst_x_k_carr: "\<And>k. k \<in> K \<Longrightarrow> fst x k \<in> carrier R" 
+    have k_carr: "k \<in> carrier R" using assms(2) b by blast
+    have fst_x_k_carr: "\<And>k. k \<in> K \<Longrightarrow> fst x k \<in> carrier R"
       using  a1 PiE_def Pi_def by blast
-    have "eval r k = eval y k \<oplus> eval w k" 
-      apply (simp add:r_def)
-      apply (subst s.hom_add[OF y_poly w_carr])
-      by (simp)
+    have "eval r k = eval y k \<oplus> eval w k"
+      using y_poly w_carr by (simp add:r_def)
     also have "... = fst x k \<ominus> local.eval w k \<oplus> local.eval w k"
-      apply (simp add:y_def)
-      apply (subst interpolate_eval[OF assms(1) assms(2) _ d])
-       apply (rule image_subsetI) using w_eval_range subsetD[OF assms(2)] fst_x_k_carr apply blast
-      by simp
+      using assms b x_minus_w_in_carrier
+      by (simp add:y_def interpolate_eval[OF _ _ image_subsetI])
+    also have "... = fst x k \<oplus> (\<ominus> local.eval w k \<oplus> local.eval w k)"
+      using fst_x_k_carr[OF b] w_eval_range[OF k_carr]
+      by (simp add:a_minus_def a_assoc)
     also have "... = fst x k"
-      using fst_x_k_carr[OF d] w_eval_range[OF k_carr]
-      apply (subst a_minus_def)
-      apply (subst a_assoc, simp, simp, simp)
-      by (simp add:a_comm r_neg) 
+      using fst_x_k_carr[OF b] w_eval_range[OF k_carr]
+      by (simp add:a_comm r_neg)
     finally show "eval r k = fst x k" by simp
   qed
 
   have "r \<in> (carrier (poly_ring R))"
-    by (rule r_poly)
-  moreover have "split_poly K r = x" 
-    apply (simp add:split_poly_def prod_eq_iff)
-    apply (rule conjI)
-     apply (rule ext, simp add:restrict_def, rule conjI, metis eval_r)
-     apply (metis PiE_E a1)
-    by (rule ext, rule coeff_r)
+    by (metis r_poly)
+  moreover have "\<And>y. (if y \<in> K then eval r y else undefined) = fst x y"
+    using a1 eval_r PiE_E by auto
+  hence "split_poly K r = x"
+    by (simp add:split_poly_def prod_eq_iff coeff_r restrict_def)
   ultimately show "x \<in> split_poly K ` (carrier (poly_ring R))"
     by blast
 qed
 
 text \<open>This is like @{thm [source] card_vimage_inj} but supports @{term "inj_on"} instead.\<close>
 lemma card_vimage_inj_on:
   assumes "inj_on f B"
   assumes "A \<subseteq> f ` B"
   shows "card (f -` A \<inter> B) = card A"
 proof -
   have "A = f ` (f -` A \<inter> B)" using assms(2) by auto
-  thus ?thesis using assms card_image 
+  thus ?thesis using assms card_image
     by (metis inf_le2 inj_on_subset)
 qed
 
 lemma inv_subsetI:
   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B \<Longrightarrow> x \<in> C"
   shows "f -` B \<inter> A \<subseteq> C"
   using assms by force
 
 text \<open>The following establishes the main result of this section: There are $\lvert F \rvert^{n-k}$
 polynomials of degree less than $n$ interpolating $k \leq n$ points.\<close>
 
+lemma restrict_eq_imp:
+  assumes "restrict f A = restrict g A"
+  assumes "x \<in> A"
+  shows "f x = g x"
+  by (metis restrict_def assms)
+
 theorem (in field) interpolating_polynomials_card:
   assumes "finite K"
   assumes "K \<subseteq> carrier R"
   assumes "f ` K \<subseteq> carrier R"
   shows "card {\<omega> \<in> bounded_degree_polynomials R (card K + n). (\<forall>k \<in> K. eval \<omega> k = f k)} = card (carrier R)^n"
     (is "card ?A = ?B")
 proof -
   define z where "z = restrict f K"
   define M where "M = {f. range f \<subseteq> carrier R \<and> (\<forall>k \<ge> n. f k = \<zero>)}"
 
   hence inj_on_bounded: "inj_on (split_poly K) (carrier (poly_ring R))"
     using split_poly_inj[OF assms(1) assms(2)] by blast
 
-  have a:"?A \<subseteq> split_poly K -` ({z} \<times> M) \<inter> carrier (poly_ring R)" 
-    apply (rule subsetI, simp add:split_poly_def z_def M_def)
-    apply (rule conjI, rule restrict_ext, simp)
-    apply (rule conjI, rule subsetI, simp add:bounded_degree_polynomials_def)
-     using coeff_in_carrier apply blast
-     apply (rule conjI, rule allI, rule impI)
-    apply (subst coeff_length, simp add:bounded_degree_polynomials_def, force, simp)
-    by (simp add:bounded_degree_polynomials_def)
+  have "?A \<subseteq> split_poly K -` ({z} \<times> M)"
+    unfolding split_poly_def z_def M_def bounded_degree_polynomials_length
+    by (rule subsetI, auto intro!:coeff_in_carrier coeff_length)
+  moreover have "?A \<subseteq> carrier (poly_ring R)"
+    unfolding bounded_degree_polynomials_length by blast
+  ultimately have a:"?A \<subseteq> split_poly K -` ({z} \<times> M) \<inter> carrier (poly_ring R)"
+    by blast
 
-  have b1: "\<And>x k . (\<lambda>k. coeff x (k + card K)) \<in> M \<Longrightarrow> k \<ge> n + card K \<Longrightarrow> coeff x k = \<zero>"
-    apply (simp add:M_def)
-    by (metis Nat.le_diff_conv2 Nat.le_imp_diff_is_add add_leD2)
+  have "\<And>x k . (\<lambda>k. coeff x (k + card K)) \<in> M \<Longrightarrow> k \<ge> n + card K \<Longrightarrow> coeff x k = \<zero>"
+    by (simp add:M_def, metis Nat.le_diff_conv2 Nat.le_imp_diff_is_add add_leD2)
+  hence "split_poly K -` ({z} \<times> M) \<inter> carrier (poly_ring R) \<subseteq> bounded_degree_polynomials R (card K + n)"
+    unfolding split_poly_def z_def using poly_degree_bound_from_coeff_1 inv_subsetI by force
+  moreover have "\<And>\<omega> k. \<omega> \<in> split_poly K -` ({z} \<times> M) \<inter> carrier (poly_ring R) \<Longrightarrow> k \<in> K \<Longrightarrow> eval \<omega> k = f k"
+    unfolding split_poly_def z_def using restrict_eq_imp by fastforce
+  ultimately have b:"split_poly K -` ({z} \<times> M) \<inter> carrier (poly_ring R) \<subseteq> ?A"
+    by blast
 
-  have b:"split_poly K -` ({z} \<times> M) \<inter> carrier (poly_ring R) \<subseteq> ?A"
-    apply (rule inv_subsetI)
-    apply (simp add:split_poly_def z_def)
-    apply (rule conjI)
-     apply (rule poly_degree_bound_from_coeff_1, simp, rule b1, simp, simp)
-    by (metis restrict_apply')
+  have "z \<in> K \<rightarrow>\<^sub>E carrier R"
+    unfolding z_def using assms(3) by auto
+  moreover have "M \<subseteq> {f. range f \<subseteq> carrier R \<and> (\<exists>n. (\<forall>k \<ge> n. f k = \<zero>))}"
+    unfolding M_def by blast
+  ultimately have c:"{z} \<times> M \<subseteq> split_poly K ` carrier (poly_ring R)"
+    using split_poly_image[OF assms(1) assms(2)] by fast
 
   have "card ?A = card (split_poly K -` ({z} \<times> M) \<inter> carrier (poly_ring R))"
-    apply (rule arg_cong[where f="card"])
-    by (rule order_antisym[OF a b])
+    using order_antisym[OF a b] by simp
   also have "... = card ({z} \<times> M)"
-    apply (rule card_vimage_inj_on[OF inj_on_bounded]) 
-    apply (rule order_trans[OF _ split_poly_image[OF assms(1) assms(2)]])
-    apply (rule subsetI, simp add:mem_Times_iff)
-    apply (simp add:z_def M_def Pi_def)
-    using assms by blast
+    using card_vimage_inj_on[OF inj_on_bounded] c by blast
   also have "... = card (carrier R)^n"
     by (simp add:card_cartesian_product M_def card_mostly_constant_maps)
   finally show ?thesis by simp
 qed
 
-text \<open>A corollary is the classic result~\cite[Theorem 7.15]{shoup2009computational} that there is 
+text \<open>A corollary is the classic result~\cite[Theorem 7.15]{shoup2009computational} that there is
 exactly one polynomial of degree less than $n$ interpolating $n$ points:\<close>
 
 corollary (in field) interpolating_polynomial_one:
   assumes "finite K"
   assumes "K \<subseteq> carrier R"
   assumes "f ` K \<subseteq> carrier R"
   shows "card {\<omega> \<in> bounded_degree_polynomials R (card K). (\<forall>k \<in> K. eval \<omega> k = f k)} = 1"
   using interpolating_polynomials_card[OF assms(1) assms(2) assms(3), where n="0"]
   by simp
 
 text \<open>In the case of fields with infinite carriers, it is possible to conclude that there are
 infinitely many polynomials of degree less than $n$ interpolating $k < n$ points.\<close>
 
 corollary (in field) interpolating_polynomial_inf:
   assumes "infinite (carrier R)"
   assumes "finite K" "K \<subseteq> carrier R" "f ` K \<subseteq> carrier R"
   assumes "n > 0"
   shows "infinite {\<omega> \<in> bounded_degree_polynomials R (card K + n). (\<forall>k \<in> K. eval \<omega> k = f k)}"
     (is "infinite ?A")
 proof -
   have "{} \<subset> {\<omega> \<in> bounded_degree_polynomials R (card K). (\<forall>k \<in> K. eval \<omega> k = f k)}"
     using interpolating_polynomial_one[OF assms(2) assms(3) assms(4)] by fastforce
   also have "... \<subseteq> ?A"
-    apply (rule subsetI)
-    apply (simp add:bounded_degree_polynomials_def)
-    by linarith
+    unfolding bounded_degree_polynomials_def by auto
   finally have a:"?A \<noteq> {}" by auto
 
   have "card ?A = card (carrier R)^n"
     using interpolating_polynomials_card[OF assms(2) assms(3) assms(4), where n="n"] by simp
   also have "... = 0"
     using assms(1) assms(5) by simp
   finally have b:"card ?A = 0" by simp
 
   show ?thesis using a b card_0_eq by blast
 qed
 
 text \<open>The following is an additional independent result: The evaluation homomorphism is injective
 for degree one polynomials.\<close>
 
 lemma  (in field) eval_inj_if_degree_1:
   assumes "p \<in> carrier (poly_ring R)" "degree p = 1"
   shows "inj_on (eval p) (carrier R)"
-proof (rule inj_onI)
-  fix x y
-  assume a1: "x \<in> carrier R"
-  assume a2: "y \<in> carrier R"
-  assume a3: "eval p x = eval p y"
-
+proof -
   obtain u v where p_def: "p = [u,v]" using assms
-    by (cases p, simp, cases "(tl p)", auto)
+    by (cases p, cases "(tl p)", auto)
 
-  have u_carr: "u \<in> carrier R - {\<zero>}" using p_def assms by blast
-  have v_carr: "v \<in> carrier R" using p_def assms by blast
-
-  show "x = y" using u_carr a1 a2 a3 v_carr
-    by (simp add: p_def local.field_Units)
+  have "u \<in> carrier R - {\<zero>}" using p_def assms by blast
+  moreover have "v \<in> carrier R" using p_def assms by blast
+  ultimately show ?thesis by (simp add:p_def field_Units inj_on_def)
 qed
 
 end
diff --git a/thys/Interpolation_Polynomials_HOL_Algebra/Lagrange_Interpolation.thy b/thys/Interpolation_Polynomials_HOL_Algebra/Lagrange_Interpolation.thy
--- a/thys/Interpolation_Polynomials_HOL_Algebra/Lagrange_Interpolation.thy
+++ b/thys/Interpolation_Polynomials_HOL_Algebra/Lagrange_Interpolation.thy
@@ -1,381 +1,358 @@
 section \<open>Lagrange Interpolation\<close>
 
 text \<open>This section introduces the function @{term "interpolate"}, which constructs the Lagrange
 interpolation polynomials for a given set of points, followed by a theorem of its correctness.\<close>
 
 theory Lagrange_Interpolation
   imports "HOL-Algebra.Polynomial_Divisibility"
 begin
 
 text \<open>A finite product in a domain is $0$ if and only if at least one factor is. This could be added
 to @{theory "HOL-Algebra.FiniteProduct"} or @{theory "HOL-Algebra.Ring"}.\<close>
 lemma (in domain) finprod_zero_iff:
   assumes "finite A"
   assumes "\<And>a. a \<in> A \<Longrightarrow> f a \<in> carrier R"
   shows "finprod R f A = \<zero> \<longleftrightarrow> (\<exists>x \<in> A. f x = \<zero>)"
   using assms
 proof (induct A rule: finite_induct)
   case empty
   then show ?case by simp
 next
   case (insert y F)
-  have a: "f \<in> F \<rightarrow> carrier R" using insert by blast
-  have b:"finprod R f F \<in> carrier R" by (rule finprod_closed[OF a])
-  have c:"f y \<in> carrier R" using insert by blast
-  have d:"(\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R)" using a by blast
-
-  show ?case
-    apply (subst comm_monoid.finprod_insert[OF comm_monoid_axioms insert(1) insert(2) a c])  
-    apply (subst integral_iff[OF c b])
-    apply (subst insert(3)[OF d], simp)
-    by blast
+  moreover have "f \<in> F \<rightarrow> carrier R" using insert by blast
+  ultimately show ?case by (simp add:integral_iff)
 qed
 
 lemma (in ring) poly_of_const_in_carrier:
   assumes "s \<in> carrier R"
   shows "poly_of_const s \<in> carrier (poly_ring R)"
-  apply (cases "s = \<zero>")
-  apply (simp add:poly_of_const_def univ_poly_zero_closed)
-  by (simp add:poly_of_const_def univ_poly_carrier[symmetric] polynomial_def assms)
+  using poly_of_const_def assms
+  by (simp add:univ_poly_carrier[symmetric] polynomial_def)
 
 lemma (in ring) eval_poly_of_const:
   assumes "x \<in> carrier R"
   shows "eval (poly_of_const x) y = x"
   using assms by (simp add:poly_of_const_def)
 
+lemma (in ring) eval_in_carrier_2:
+  assumes "x \<in> carrier (poly_ring R)"
+  assumes "y \<in> carrier R"
+  shows "eval x y \<in> carrier R"
+  using eval_in_carrier univ_poly_carrier polynomial_incl assms by blast
+
+lemma (in domain) poly_mult_degree_le_1:
+  assumes "x \<in> carrier (poly_ring R)"
+  assumes "y \<in> carrier (poly_ring R)"
+  shows "degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> degree x + degree y"
+proof -
+  have "degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)"
+    unfolding univ_poly_mult
+    by (metis univ_poly_carrier assms(1,2) carrier_is_subring poly_mult_degree_eq)
+  thus ?thesis by (metis nat_le_linear zero_le)
+qed
+
 lemma (in domain) poly_mult_degree_le:
   assumes "x \<in> carrier (poly_ring R)"
   assumes "y \<in> carrier (poly_ring R)"
   assumes "degree x \<le> n"
   assumes "degree y \<le> m"
   shows "degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> n + m"
-proof -
-  have a: "polynomial\<^bsub>R\<^esub> (carrier R) x" using assms 
-    by (meson univ_poly_carrier)
-  have b: "polynomial\<^bsub>R\<^esub> (carrier R) y" using assms 
-    by (meson univ_poly_carrier)
-  have c: "subring (carrier R) R" by (simp add: carrier_is_subring)
-  have "degree (ring.poly_mult R x y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)"
-    using a b c poly_mult_degree_eq by blast
-  hence "degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)"
-    by (simp add: univ_poly_mult)
-  thus ?thesis using assms 
-    by (metis add_mono_thms_linordered_semiring(1) zero_le)   
-qed
+  using poly_mult_degree_le_1 assms add_mono by force
 
 lemma (in domain) poly_add_degree_le:
   assumes "x \<in> carrier (poly_ring R)" "degree x \<le> n"
   assumes "y \<in> carrier (poly_ring R)" "degree y \<le> n"
   shows "degree (x \<oplus>\<^bsub>poly_ring R\<^esub> y) \<le> n"
-proof -
-  have "degree (x \<oplus>\<^bsub>poly_ring R\<^esub> y) \<le> n" using assms poly_add_degree 
-    by (metis dual_order.trans max.bounded_iff univ_poly_add)
-  then show ?thesis using assms by linarith
-qed
+  using assms poly_add_degree
+  by (metis dual_order.trans max.bounded_iff univ_poly_add)
 
 lemma (in domain) poly_sub_degree_le:
   assumes "x \<in> carrier (poly_ring R)" "degree x \<le> n"
   assumes "y \<in> carrier (poly_ring R)" "degree y \<le> n"
   shows "degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n"
 proof -
-  interpret x:cring "poly_ring R" 
+  interpret x:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
 
   show ?thesis
-    apply (subst a_minus_def)
-    apply (rule poly_add_degree_le[OF assms(1) assms(2)])
-     apply (rule x.a_inv_closed[OF assms(3)])
-    apply (subst univ_poly_a_inv_degree[OF carrier_is_subring assms(3)])
-    by (rule assms(4)) 
+    unfolding a_minus_def
+    using assms univ_poly_a_inv_degree carrier_is_subring poly_add_degree_le x.a_inv_closed
+    by simp
 qed
 
 lemma (in domain) poly_sum_degree_le:
   assumes "finite A"
   assumes "\<And>x. x \<in> A \<Longrightarrow> degree (f x) \<le> n"
   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> carrier (poly_ring R)"
   shows "degree (finsum (poly_ring R) f A) \<le> n"
   using assms
 proof (induct A rule:finite_induct)
   case empty
-  interpret x:cring "poly_ring R" 
+  interpret x:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
   show ?case using empty by (simp add:univ_poly_zero)
 next
   case (insert x F)
-  interpret x:cring "poly_ring R" 
+  interpret x:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
   have a: "degree (f x \<oplus>\<^bsub>poly_ring R\<^esub> finsum (poly_ring R) f F) \<le> n"
-    apply (rule poly_add_degree_le)
-    using insert  x.finsum_closed by auto
-  show ?case
-    apply (subst x.finsum_insert[OF insert(1) insert(2)])
-    using insert a by auto
+    using insert poly_add_degree_le x.finsum_closed by auto
+  show ?case using insert a by auto
 qed
 
-definition (in ring) lagrange_basis_polynomial_aux where 
-  "lagrange_basis_polynomial_aux S = 
+definition (in ring) lagrange_basis_polynomial_aux where
+  "lagrange_basis_polynomial_aux S =
     (\<Otimes>\<^bsub>poly_ring R\<^esub> s \<in> S. X \<ominus>\<^bsub>poly_ring R\<^esub> (poly_of_const s))"
 
 lemma (in domain) lagrange_aux_eval:
   assumes "finite S"
   assumes "S \<subseteq> carrier R"
   assumes "x \<in> carrier R"
   shows "(eval (lagrange_basis_polynomial_aux S) x) = (\<Otimes>s \<in> S. x \<ominus> s)"
 proof -
   interpret x:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p x)"
     by (rule eval_cring_hom[OF carrier_is_subring assms(3)])
 
-  have a: "\<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)"
-    by (meson poly_of_const_in_carrier carrier_is_subring assms(2) cring.cring_simprules(4) 
+  have "\<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)"
+    by (meson poly_of_const_in_carrier carrier_is_subring assms(2) cring.cring_simprules(4)
         domain_def subsetD univ_poly_is_domain var_closed(1))
 
-  have b:"\<And>s. s \<in> S \<Longrightarrow> eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const s) x = x \<ominus> s"
-    apply (subst x.hom_sub, rule var_closed(1)[OF carrier_is_subring])
-     apply (rule poly_of_const_in_carrier, rule subsetD[OF assms(2)], simp)
-    apply (subst eval_var[OF assms(3)])
-    apply (subst eval_poly_of_const, metis subsetD[OF assms(2)])
-    by simp
+  moreover have "\<And>s. s \<in> S \<Longrightarrow> eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const s) x = x \<ominus> s"
+    using assms var_closed carrier_is_subring poly_of_const_in_carrier subsetD[OF assms(2)]
+    by (simp add:eval_var eval_poly_of_const)
 
-  have c:"a_minus R x \<in> S \<rightarrow> carrier R"
+  moreover have "a_minus R x \<in> S \<rightarrow> carrier R"
     using assms by blast
 
-  show ?thesis
-    apply (simp add:lagrange_basis_polynomial_aux_def)
-    apply (subst x.hom_finprod, rule Pi_I, erule a)
-    apply (rule finprod_cong', simp, simp add:c)
-    by (simp add:b)
+  ultimately show ?thesis
+    by (simp add:lagrange_basis_polynomial_aux_def x.hom_finprod cong:finprod_cong')
 qed
 
 lemma (in domain) lagrange_aux_poly:
   assumes "finite S"
   assumes "S \<subseteq> carrier R"
   shows "lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)"
 proof -
-  have a:"subring (carrier R) R"  
+  have a:"subring (carrier R) R"
     using carrier_is_subring assms by blast
 
-  have b: "\<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)" 
+  have b: "\<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)"
     by (meson poly_of_const_in_carrier a assms(2) cring.cring_simprules(4) domain_def subsetD
         univ_poly_is_domain var_closed(1))
 
-  interpret x:cring "poly_ring R" 
+  interpret x:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
 
   show ?thesis
-    apply (simp add:lagrange_basis_polynomial_aux_def)
-    apply (rule x.finprod_closed)
-    by (rule Pi_I, rule b, simp)
+    using lagrange_basis_polynomial_aux_def b x.finprod_closed[OF Pi_I] by simp
+qed
+
+lemma (in domain) poly_prod_degree_le:
+  assumes "finite A"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> carrier (poly_ring R)"
+  shows "degree (finprod (poly_ring R) f A) \<le> (\<Sum>x \<in> A. degree (f x))"
+  using assms
+proof (induct A rule:finite_induct)
+  case empty
+  interpret x:cring "poly_ring R"
+    using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
+  show ?case by (simp add:univ_poly_one)
+next
+  case (insert x F)
+  interpret x:cring "poly_ring R"
+    using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
+  have a:"f \<in> F \<rightarrow> carrier (poly_ring R)"
+    using insert by blast
+  have b:"f x \<in> carrier (poly_ring R)"
+    using insert by blast
+  have "degree (finprod (poly_ring R) f (insert x F)) = degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F)"
+    using a b insert by simp
+  also have "... \<le> degree (f x) + degree (finprod (poly_ring R) f F)"
+    using poly_mult_degree_le x.finprod_closed[OF a] b by auto
+  also have "... \<le> degree (f x) + (\<Sum>y \<in> F. degree (f y))"
+    using insert(3) a add_mono by auto
+  also have "... = (\<Sum>y \<in> (insert x F). degree (f y))" using insert by simp
+  finally show ?case by simp
 qed
 
 lemma (in domain) lagrange_aux_degree:
   assumes "finite S"
   assumes "S \<subseteq> carrier R"
   shows "degree (lagrange_basis_polynomial_aux S) \<le> card S"
-  using assms
-proof (induct S rule: finite_induct)
-  case empty
-  interpret x:cring "poly_ring R" 
+proof -
+  interpret x:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
-  show ?case using empty by (simp add:lagrange_basis_polynomial_aux_def univ_poly_one)
-next
-  case (insert x F)
-  interpret x:cring "poly_ring R" 
-    using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
-  have a:"subring (carrier R) R"  
-    using carrier_is_subring assms by blast
-
-  have b: "\<And>a. a \<in> carrier R \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)"
-    by (meson poly_of_const_in_carrier a cring.cring_simprules(4) domain_def subsetD
-        univ_poly_is_domain var_closed(1))
 
-  have c:"F \<subseteq> carrier R" using insert by blast
-  have d:"x \<in> carrier R" using insert by blast
-  have e: "degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const x) \<le> 1"
-    apply (rule poly_sub_degree_le, rule var_closed(1)[OF a])
-    apply (simp add:var_def)
-    using d poly_of_const_in_carrier apply blast
-    by (simp add:poly_of_const_def)
+  have "degree X \<le> 1" by (simp add:var_def)
+  moreover have "\<And>y. y\<in> S \<Longrightarrow> degree (poly_of_const y) \<le> 1" by (simp add:poly_of_const_def)
+  ultimately have a: "\<And>y. y\<in> S \<Longrightarrow> degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y) \<le> 1"
+    by (meson assms(2) in_mono poly_of_const_in_carrier poly_sub_degree_le var_closed[OF carrier_is_subring])
 
-  have "degree (lagrange_basis_polynomial_aux (insert x F)) \<le> 
-    1 + card F"
-    apply (subst lagrange_basis_polynomial_aux_def)
-    apply (subst x.finprod_insert[OF insert(1) insert(2)])
-      apply (rule Pi_I, rule b, metis subsetD[OF c])
-     apply (rule b, rule d)
-    apply (rule poly_mult_degree_le[OF b[OF d]])
-      apply (rule x.finprod_closed, rule Pi_I, rule b, metis subsetD[OF c])
-     apply (rule e)
-    using insert(3)[OF c] lagrange_basis_polynomial_aux_def by simp
-  also have "... \<le> card (insert x F)" using insert by simp
-  finally show ?case by simp 
+  have b:"\<And>y. y \<in> S \<Longrightarrow> (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y) \<in> carrier (poly_ring R)"
+    by (meson subsetD x.minus_closed var_closed(1)[OF carrier_is_subring] poly_of_const_in_carrier assms(2))
+
+  have "degree (lagrange_basis_polynomial_aux S) \<le> (\<Sum>y \<in> S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y))"
+    using lagrange_basis_polynomial_aux_def b poly_prod_degree_le[OF assms(1)] by auto
+  also have "... \<le> (\<Sum>y \<in> S. 1)"
+    using sum_mono a by force
+  also have "... = card S" by simp
+  finally show ?thesis by simp
 qed
 
-definition (in ring) lagrange_basis_polynomial where 
+definition (in ring) lagrange_basis_polynomial where
   "lagrange_basis_polynomial S x = lagrange_basis_polynomial_aux S
     \<otimes>\<^bsub>poly_ring R\<^esub> (poly_of_const (inv\<^bsub>R\<^esub> (\<Otimes>s \<in> S. x \<ominus> s)))"
 
-lemma (in field) 
+lemma (in field)
   assumes "finite S"
   assumes "S \<subseteq> carrier R"
   assumes "x \<in> carrier R - S"
-  shows 
+  shows
     lagrange_one: "eval (lagrange_basis_polynomial S x) x = \<one>" and
     lagrange_degree: "degree (lagrange_basis_polynomial S x) \<le> card S" and
     lagrange_zero: "\<And>s. s \<in> S \<Longrightarrow> eval (lagrange_basis_polynomial S x) s = \<zero>" and
     lagrange_poly: "lagrange_basis_polynomial S x \<in> carrier (poly_ring R)"
 proof -
-  have a:"subring (carrier R) R"  
-    using carrier_is_subring assms by blast
-
   interpret x:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p x)"
-    apply (rule eval_cring_hom[OF a]) using assms by blast
+    using assms carrier_is_subring eval_cring_hom by blast
 
   define p where "p = lagrange_basis_polynomial_aux S"
-  have b:"p \<in> carrier (poly_ring R)"
-    apply (simp add:p_def)
-    by (rule lagrange_aux_poly[OF assms(1) assms(2)])
+  have a:"eval p x = (\<Otimes>s \<in> S. x \<ominus> s)"
+    using assms by (simp add:p_def lagrange_aux_eval)
 
-  have c:"eval p x = (\<Otimes>s \<in> S. x \<ominus> s)"
-    apply (simp add:p_def)
-    apply (subst lagrange_aux_eval[OF assms(1) assms(2)])
-    using assms(3) by auto
+  have b:"p \<in> carrier (poly_ring R)" using assms
+    by (simp add:p_def lagrange_aux_poly)
 
-  have d:"a_minus R x \<in> S \<rightarrow> carrier R"
+  have "\<And>y. y \<in> S \<Longrightarrow> a_minus R x y \<in> carrier R"
     using assms by blast
 
-  have e:"finprod R (a_minus R x) S \<in> Units R"
-    apply (simp add:field_Units)
-    apply (rule conjI, rule finprod_closed[OF d])
-    apply (subst finprod_zero_iff[OF assms(1)])
-    using assms by auto
+  hence c:"finprod R (a_minus R x) S \<in> Units R"
+    using finprod_closed[OF Pi_I] assms
+    by (auto simp add:field_Units finprod_zero_iff)
 
-  show "eval (lagrange_basis_polynomial S x) x = \<one>"
-    apply (simp add:lagrange_basis_polynomial_def Let_def p_def[symmetric])
-    apply (subst x.hom_mult[OF b])
-     apply (rule poly_of_const_in_carrier)
-     apply (rule Units_inv_closed, rule e)
-    apply (simp add:c)
-    apply (subst eval_poly_of_const, rule Units_inv_closed[OF e])
-    using e Units_r_inv by blast
+  have "eval (lagrange_basis_polynomial S x) x =
+    (\<Otimes>s \<in> S. x \<ominus> s) \<otimes> eval (poly_of_const (inv finprod R (a_minus R x) S)) x"
+    using poly_of_const_in_carrier Units_inv_closed c p_def[symmetric]
+    by (simp add: lagrange_basis_polynomial_def x.hom_mult[OF b] a)
+  also have "... =  \<one>"
+    using poly_of_const_in_carrier Units_inv_closed c eval_poly_of_const by simp
+  finally show "eval (lagrange_basis_polynomial S x) x = \<one>" by simp
 
-  show "degree (lagrange_basis_polynomial S x) \<le> card S"
-    apply (simp add:lagrange_basis_polynomial_def Let_def p_def[symmetric])
-    apply (rule poly_mult_degree_le[where m="0",simplified], rule b)
-      apply (rule poly_of_const_in_carrier, rule Units_inv_closed, rule e)
-     apply (simp add:p_def lagrange_aux_degree[OF assms(1) assms(2), simplified])
-    by (simp add:poly_of_const_def)
+  have "degree (lagrange_basis_polynomial S x) \<le> degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))"
+    unfolding lagrange_basis_polynomial_def p_def[symmetric]
+    using poly_mult_degree_le[OF b] poly_of_const_in_carrier Units_inv_closed c by auto
+  also have "... \<le> card S + 0"
+    using add_mono lagrange_aux_degree[OF assms(1) assms(2)] p_def poly_of_const_def by auto
+  finally show "degree (lagrange_basis_polynomial S x) \<le> card S" by simp
 
   show "\<And>s. s \<in> S \<Longrightarrow> eval (lagrange_basis_polynomial S x) s = \<zero>"
   proof -
     fix s
-    assume f:"s \<in> S"
-    have g:"eval p s = \<zero>\<^bsub>R\<^esub>"
-      apply (simp add:p_def)
-      apply (subst lagrange_aux_eval[OF assms(1) assms(2)])
-      apply (meson in_mono f assms)
-      apply (subst finprod_zero_iff[OF assms(1)])
-      using assms f apply blast
-      by (meson assms f in_mono r_right_minus_eq)
+    assume d:"s \<in> S"
 
     interpret s:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p s)"
-      apply (rule eval_cring_hom[OF a]) using assms f by blast
-    have h:"eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R"
-      apply (rule s.hom_closed, rule poly_of_const_in_carrier)
-      by (rule Units_inv_closed,  rule e)
+      using eval_cring_hom carrier_is_subring assms d by blast
 
-    show "eval (lagrange_basis_polynomial S x) s = \<zero>"
-      apply (simp add:lagrange_basis_polynomial_def Let_def p_def[symmetric])
-      apply (subst s.hom_mult[OF b])
-       apply (rule poly_of_const_in_carrier)
-       apply (rule Units_inv_closed, rule e)
-      by (simp add:g h)
+    have "eval p s = finprod R (a_minus R s) S"
+      using subsetD[OF assms(2) d] assms
+      by (simp add:p_def lagrange_aux_eval)
+    also have "... = \<zero>"
+      using subsetD[OF assms(2)] d assms by (simp add: finprod_zero_iff)
+    finally have "eval p s = \<zero>\<^bsub>R\<^esub>" by simp
+
+    moreover have "eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R"
+      using s.hom_closed poly_of_const_in_carrier  Units_inv_closed c by blast
+
+    ultimately show "eval (lagrange_basis_polynomial S x) s = \<zero>"
+      using poly_of_const_in_carrier Units_inv_closed c
+      by (simp add:lagrange_basis_polynomial_def Let_def p_def[symmetric] s.hom_mult[OF b])
   qed
 
   interpret r:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
 
   show "lagrange_basis_polynomial S x \<in> carrier (poly_ring R)"
-    apply (simp add:lagrange_basis_polynomial_def Let_def p_def[symmetric])
-    using poly_of_const_in_carrier[OF Units_inv_closed] c e b
-    by simp
+    using lagrange_basis_polynomial_def p_def[symmetric] poly_of_const_in_carrier Units_inv_closed
+      a b c by simp
 qed
 
-definition (in ring) interpolate where 
-  "interpolate S f = 
+definition (in ring) interpolate where
+  "interpolate S f =
    (\<Oplus>\<^bsub>poly_ring R\<^esub>s \<in> S. lagrange_basis_polynomial (S - {s}) s \<otimes>\<^bsub>poly_ring R\<^esub> (poly_of_const (f s)))"
 
 text \<open>Let @{term "f"} be a function and @{term "S"} be a finite subset of the domain of the field.
 Then @{term "interpolate S f"} will return a polynomial with degree less than @{term "card S"}
 interpolating @{term "f"} on @{term "S"}.\<close>
 
 theorem (in field)
   assumes "finite S"
   assumes "S \<subseteq> carrier R"
   assumes "f ` S \<subseteq> carrier R"
-  shows 
+  shows
     interpolate_poly: "interpolate S f \<in> carrier (poly_ring R)" and
     interpolate_degree: "degree (interpolate S f) \<le> card S - 1" and
     interpolate_eval: "\<And>s. s \<in> S \<Longrightarrow> eval (interpolate S f) s = f s"
 proof -
   interpret r:cring "poly_ring R"
     using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
 
   have a:"\<And>x. x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {x}) x \<in> carrier (poly_ring R)"
     by (meson lagrange_poly assms Diff_iff finite_Diff in_mono insertI1 subset_insertI2 subset_insert_iff)
 
   have b:"\<And>x. x \<in> S \<Longrightarrow> f x \<in> carrier R" using assms by blast
 
   have c:"\<And>x. x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {x}) x) \<le> card S - 1"
-    by (metis (full_types) lagrange_degree  DiffI Diff_insert_absorb assms(1) assms(2) 
+    by (metis (full_types) lagrange_degree  DiffI Diff_insert_absorb assms(1) assms(2)
         card_Diff_singleton finite_insert insert_subset mk_disjoint_insert)
 
+  have d: "\<And>x. x \<in> S \<Longrightarrow>
+    degree (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) \<le> (card S - 1) + 0"
+    using poly_of_const_in_carrier[OF b] poly_mult_degree_le[OF a] c poly_of_const_def by fastforce
+
   show "interpolate S f \<in> carrier (poly_ring R)"
-    apply (simp add:interpolate_def)
-    apply (rule r.finsum_closed)
-    apply (rule Pi_I)
-    using poly_of_const_in_carrier[OF b] a by simp
+    using interpolate_def poly_of_const_in_carrier a b by simp
 
   show "degree (interpolate S f) \<le> card S - 1"
-    apply (subst interpolate_def)
-    apply (rule poly_sum_degree_le[OF assms(1)])
-     apply (rule order_trans[where y="(card S - 1) + 0"])
-      apply (rule poly_mult_degree_le[OF a], simp, rule poly_of_const_in_carrier[OF b], simp, rule c, simp)
-      apply (simp add:poly_of_const_def)
-     apply simp
-    using poly_of_const_in_carrier[OF b] a by simp
+    using poly_sum_degree_le[OF assms(1) d] poly_of_const_in_carrier[OF b] interpolate_def a by simp
 
   have e:"subring (carrier R) R"
     using carrier_is_subring assms by blast
 
   show "\<And>s. s \<in> S \<Longrightarrow> eval (interpolate S f) s = f s"
   proof -
     fix s
-    assume d:"s \<in> S"
+    assume f:"s \<in> S"
     interpret s:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p s)"
-      apply (rule eval_cring_hom[OF e]) using assms d by blast
-    have e:"\<And>i. i \<in> S \<Longrightarrow>
+      using eval_cring_hom[OF e] assms f by blast
+    have g:"\<And>i. i \<in> S \<Longrightarrow>
          eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s =
          (if s = i then f s else \<zero>)"
-      apply (subst s.hom_mult[OF a], simp, rule poly_of_const_in_carrier, rule b, simp)
-      apply (simp add:eval_poly_of_const b)
-      apply (rule conjI, rule impI, subst lagrange_one, simp add:assms)
-         using assms apply blast
-        using assms apply blast
-       apply (simp add:b)
-      apply (rule impI, subst lagrange_zero, simp add:assms)
-      using assms d by auto
+    proof -
+      fix i
+      assume i_in_S: "i \<in> S"
+      have "eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s =
+        eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i"
+        using b i_in_S poly_of_const_in_carrier
+        by (simp add: s.hom_mult[OF a] eval_poly_of_const)
+      also have "... = (if s = i then f s else \<zero>)"
+        using b i_in_S poly_of_const_in_carrier assms f
+        apply (cases "s=i", simp, subst lagrange_one, auto)
+        by (subst lagrange_zero, auto)
+      finally show
+        "eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s =
+         (if s = i then f s else \<zero>)" by simp
+    qed
 
-    have "eval (interpolate S f) s = (\<Oplus>x\<in>S. if s = x then f s else \<zero>)"
-      apply (subst interpolate_def)
-      apply (subst s.hom_finsum, simp add:Pi_def poly_of_const_in_carrier[OF b] a)
-      apply (simp add:comp_def)
-      apply (rule finsum_cong', simp, simp add:Pi_def b)
-      by (rule e, simp)
+    have "eval (interpolate S f) s =
+    (\<Oplus>x\<in>S. eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s)"
+      using  poly_of_const_in_carrier[OF b] a e
+      by (simp add: interpolate_def s.hom_finsum[OF Pi_I] comp_def)
+    also have "... =  (\<Oplus>x\<in>S. if s = x then f s else \<zero>)"
+      using b g by (simp cong: finsum_cong)
     also have "... = f s"
-      apply (rule finsum_singleton[OF d assms(1)])
-      using d assms by blast
+      using finsum_singleton[OF f assms(1)] f assms by auto
     finally show "eval (interpolate S f) s = f s" by simp
   qed
 qed
 
 end
\ No newline at end of file