diff -r 4069afca81fd -r f831b6e589dc src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sat Oct 30 13:26:33 2021 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Sat Oct 30 17:10:10 2021 +0200
@@ -1175,14 +1175,15 @@
 
 (* Contributed by Dominique Unruh *)
 lemma ennreal_of_enat_plus[simp]: \<open>ennreal_of_enat (a+b) = ennreal_of_enat a + ennreal_of_enat b\<close>
-  apply (induction a)
-  apply auto
-  by (smt (z3) add.commute add.right_neutral enat.exhaust enat.simps(4) enat.simps(5) ennreal_add_left_cancel ennreal_of_enat_def infinity_ennreal_def of_nat_add of_nat_eq_enat plus_enat_simps(2))
+  apply (induct a)
+   apply (metis enat.exhaust ennreal_add_eq_top ennreal_of_enat_enat ennreal_of_enat_infty infinity_ennreal_def of_nat_add plus_enat_simps(1) plus_eq_infty_iff_enat)
+  apply simp
+  done
 
 (* Contributed by Dominique Unruh *)
 lemma sum_ennreal_of_enat[simp]: "(\<Sum>i\<in>I. ennreal_of_enat (f i)) = ennreal_of_enat (sum f I)"
-  apply (induction I rule: infinite_finite_induct) 
-  by (auto simp: sum_nonneg)
+  by (induct I rule: infinite_finite_induct) (auto simp: sum_nonneg)
+
 
 subsection \<open>Topology on \<^typ>\<open>ennreal\<close>\<close>