[STATEMENT]
lemma DERIV_LIM_iff:
  fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a"
  shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D = (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D \<Longrightarrow> (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
 2. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D

goal (2 subgoals):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D \<Longrightarrow> (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
 2. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
have "(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>0 - - a\<rightarrow> D"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D
[PROOF STEP]
by (rule LIM_offset)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D

goal (2 subgoals):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D \<Longrightarrow> (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
 2. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
[PROOF STEP]
have "(\<lambda>x. (f (x+a) - f a) / ((x+a) - a)) \<midarrow>a-a\<rightarrow> D"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D
[PROOF STEP]
by (rule LIM_offset)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D

goal:
No subgoals!
[PROOF STEP]
qed