src/HOL/Analysis/Derivative.thy

     by (metis trivial_limit_within)
   show ?thesis
     apply (rule linear_eq_stdbasis)
     unfolding linear_conv_bounded_linear
     apply (rule as(1,2)[THEN conjunct1])+
-  proof (rule, rule ccontr)
+  proof (rule ccontr)
     fix i :: 'a
     assume i: "i \<in> Basis"
     define e where "e = norm (f' i - f'' i)"
     assume "f' i \<noteq> f'' i"
     then have "e > 0"

 text \<open>Hence the following eccentric variant of the inverse function theorem.
   This has no continuity assumptions, but we do need the inverse function.
   We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
   algebra theory I've set up so far.\<close>
 
-(* move  before left_inverse_linear in Euclidean_Space*)
-
-lemma right_inverse_linear:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes lf: "linear f"
-    and gf: "f \<circ> g = id"
-  shows "linear g"
-proof -
-  from gf have fi: "surj f"
-    by (auto simp add: surj_def o_def id_def) metis
-  from linear_surjective_isomorphism[OF lf fi]
-  obtain h:: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
-    by blast
-  have "h = g"
-    apply (rule ext)
-    using gf h(2,3)
-    apply (simp add: o_def id_def fun_eq_iff)
-    apply metis
-    done
-  with h(1) show ?thesis by blast
-qed
-
 lemma has_derivative_inverse_strong:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   assumes "open s"
     and "x \<in> s"
     and "continuous_on s f"

     by (metis eventually_gt_at_top)
   then have
     "\<forall>\<^sub>F n in sequentially. ((\<lambda>x. \<Sum>i<n. ?e i x) \<longlongrightarrow> A) ?F"
     by eventually_elim
       (auto intro!: tendsto_eq_intros
-        simp: power_0_left if_distrib cond_application_beta sum.delta
+        simp: power_0_left if_distrib if_distribR sum.delta
         cong: if_cong)
   ultimately
   have [tendsto_intros]: "((\<lambda>x. \<Sum>i. ?e i x) \<longlongrightarrow> A) ?F"
     by (auto intro!: swap_uniform_limit[where f="\<lambda>n x. \<Sum>i < n. ?e i x" and F = sequentially])
   have [tendsto_intros]: "((\<lambda>x. if x = t then 0 else 1) \<longlongrightarrow> 1) ?F"