src/HOL/Library/FuncSet.thy
 changeset 63092 a949b2a5f51d parent 63060 293ede07b775 child 64910 6108dddad9f0
1.1 --- a/src/HOL/Library/FuncSet.thy	Fri May 13 20:22:02 2016 +0200
1.2 +++ b/src/HOL/Library/FuncSet.thy	Fri May 13 20:24:10 2016 +0200
1.3 @@ -402,17 +402,17 @@
1.4  proof -
1.5    {
1.6      fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
1.7 -    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.8 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.9        by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
1.10    }
1.11    moreover
1.12    {
1.13      fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
1.14 -    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.15 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.16        by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
1.17    }
1.18    ultimately show ?thesis
1.19 -    using assms by (auto intro: PiE_fun_upd)
1.20 +    by (auto intro: PiE_fun_upd)
1.21  qed
1.23  lemma PiE_Int: "Pi\<^sub>E I A \<inter> Pi\<^sub>E I B = Pi\<^sub>E I (\<lambda>x. A x \<inter> B x)"