diff -r 79fab5ff4163 -r e349c2da30d2 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Tue Feb 22 21:34:29 2022 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Wed Feb 23 16:28:37 2022 +0000
@@ -81,41 +81,13 @@
 unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
 
 lemma Cnotzero_cexp:
-  assumes "Cnotzero q" "Card_order r"
+  assumes "Cnotzero q" 
   shows "Cnotzero (q ^c r)"
-proof (cases "r =o czero")
-  case False thus ?thesis
-    apply -
-    apply (rule Cnotzero_mono)
-    apply (rule assms(1))
-    apply (rule Card_order_cexp)
-    apply (rule ordLeq_cexp1)
-    apply (rule conjI)
-    apply (rule notI)
-    apply (erule notE)
-    apply (rule ordIso_transitive)
-    apply assumption
-    apply (rule czero_ordIso)
-    apply (rule assms(2))
-    apply (rule conjunct2)
-    apply (rule assms(1))
-  done
-next
-  case True thus ?thesis
-    apply -
-    apply (rule Cnotzero_mono)
-    apply (rule cone_Cnotzero)
-    apply (rule Card_order_cexp)
-    apply (rule ordIso_imp_ordLeq)
-    apply (rule ordIso_symmetric)
-    apply (rule ordIso_transitive)
-    apply (rule cexp_cong2)
-    apply assumption
-    apply (rule conjunct2)
-    apply (rule assms(1))
-    apply (rule assms(2))
-    apply (rule cexp_czero)
-  done
+proof -
+  have "Field q \<noteq> {}"
+    by (metis Card_order_iff_ordIso_card_of assms(1) czero_def)
+  then show ?thesis
+    by (simp add: card_of_ordIso_czero_iff_empty cexp_def)
 qed
 
 lemma Cinfinite_ctwo_cexp:
@@ -156,31 +128,10 @@
 
 lemma csum_cexp: "\<lbrakk>Cinfinite r1; Cinfinite r2; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow>
   q ^c r1 +c q ^c r2 \<le>o q ^c (r1 +c r2)"
-apply (rule csum_cinfinite_bound)
-apply (rule cexp_mono2)
-apply (rule ordLeq_csum1)
-apply (erule conjunct2)
-apply assumption
-apply (rule notE)
-apply (rule cinfinite_not_czero[of r1])
-apply (erule conjunct1)
-apply assumption
-apply (erule conjunct2)
-apply (rule cexp_mono2)
-apply (rule ordLeq_csum2)
-apply (erule conjunct2)
-apply assumption
-apply (rule notE)
-apply (rule cinfinite_not_czero[of r2])
-apply (erule conjunct1)
-apply assumption
-apply (erule conjunct2)
-apply (rule Card_order_cexp)
-apply (rule Card_order_cexp)
-apply (rule Cinfinite_cexp)
-apply assumption
-apply (rule Cinfinite_csum)
-by (rule disjI1)
+  apply (rule csum_cinfinite_bound)
+  apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum1)
+  apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum2)
+  by (simp_all add: Card_order_cexp Cinfinite_csum1 Cinfinite_cexp cinfinite_cexp)
 
 lemma csum_cexp': "\<lbrakk>Cinfinite r; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow> q +c r \<le>o q ^c r"
 apply (rule csum_cinfinite_bound)