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.22  
    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)"