Применяя лемму решить задачу

Question

Я пытаюсь доказать следующую лемму, используя теорему

lemma lm22: 
fixes f :: "real ⇒ 'a::banach" 
assumes "a ≤ b" 
and "∀x∈{a .. b}. (f has_vector_derivative f' x) (at x within {a .. b} 
shows "(f' has_integral (f b - f a)) {a .. b}" 

вывода Isabelle состояния, что цель может быть решена непосредственно с Integration.fundamental_theorem_of_calculus. Однако добавление:

using fundamental_theorem_of_calculus [of a b f f'] by auto 

не работает. Я попытался определить a и b, а также заменить переменные значениями, но не добился успеха.

Как я могу применить лемму для доказательства цели?

Answer 1

решения прямые особенность Изабелла рассматривает предположения из assumes положений, но такие предположения не доступны для доказательства методов, таких как by auto, если вы явно не приковать их. Написать using assms перед остальной частью вашего доказательства, и он должен пройти.