src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

 lemma affinity_inverses:
   assumes m0: "m \<noteq> (0::'a::field)"
   shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
   "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
   using m0
-  apply (auto simp add: fun_eq_iff vector_add_ldistrib)
-  apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
+  apply (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
+  apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1 [symmetric])
   done
 
 lemma vector_affinity_eq:
   assumes m0: "(m::'a::field) \<noteq> 0"
   shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"

   hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
   then show "x = inverse m *s y + - (inverse m *s c)"
     using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
 next
   assume h: "x = inverse m *s y + - (inverse m *s c)"
-  show "m *s x + c = y" unfolding h diff_minus[symmetric]
+  show "m *s x + c = y" unfolding h
     using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
 qed
 
 lemma vector_eq_affinity:
     "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"