[STATEMENT]
lemma take_n:
  fixes n :: nat and l :: "'a list" and g :: "'a list"
  assumes "take n l = take n g" and "Suc n \<le> length g" and "length l = length g"
  shows "take (Suc n) (l[n := g!n]) = take (Suc n) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
Suc n \<le> length g
[PROOF STEP]
have ng: "n < length g"
[PROOF STATE]
proof (prove)
using this:
Suc n \<le> length g

goal (1 subgoal):
 1. n < length g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < length g

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
length l = length g
n < length g
[PROOF STEP]
have nlupd: "n < length (l[n := g!n])"
[PROOF STATE]
proof (prove)
using this:
length l = length g
n < length g

goal (1 subgoal):
 1. n < length (l[n := g ! n])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < length (l[n := g ! n])

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
hence nl: "n < length l"
[PROOF STATE]
proof (prove)
using this:
n < length (l[n := g ! n])

goal (1 subgoal):
 1. n < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < length l

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
from 
    sym[OF assms(1)] id_take_nth_drop[OF ng] take_Suc_conv_app_nth[OF nlupd]
    nth_list_update_eq[OF nl] take_Suc_conv_app_nth[OF ng]
    upd_conv_take_nth_drop[OF nl] assms(2-3)
[PROOF STATE]
proof (chain)
picking this:
take n g = take n l
g = take n g @ g ! n # drop (Suc n) g
take (Suc n) (l[n := g ! n]) = take n (l[n := g ! n]) @ [l[n := g ! n] ! n]
l[n := ?x] ! n = ?x
take (Suc n) g = take n g @ [g ! n]
l[n := ?a] = take n l @ ?a # drop (Suc n) l
Suc n \<le> length g
length l = length g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take n g = take n l
g = take n g @ g ! n # drop (Suc n) g
take (Suc n) (l[n := g ! n]) = take n (l[n := g ! n]) @ [l[n := g ! n] ! n]
l[n := ?x] ! n = ?x
take (Suc n) g = take n g @ [g ! n]
l[n := ?a] = take n l @ ?a # drop (Suc n) l
Suc n \<le> length g
length l = length g

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take (Suc n) (l[n := g ! n]) = take (Suc n) g

goal:
No subgoals!
[PROOF STEP]
qed