case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
⊢ init (update q (↑castSucc i) y) j = update (init q) i y j
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
⊢ init (update q (↑castSucc i) y) = update (init q) i y
ext j
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
h : j = i
⊢ init (update q (↑castSucc i) y) j = update (init q) i y j

case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
h : ¬j = i
⊢ init (update q (↑castSucc i) y) j = update (init q) i y j
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
⊢ init (update q (↑castSucc i) y) j = update (init q) i y j
by_cases h : j = i
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
h : j = i
⊢ init (update q (↑castSucc i) y) i = update (init q) i y i
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
h : j = i
⊢ init (update q (↑castSucc i) y) j = update (init q) i y j
rw [h]
no goals
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
h : j = i
⊢ init (update q (↑castSucc i) y) i = update (init q) i y i
simp [init]
no goals
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
j : Fin n
h : ¬j = i
⊢ init (update q (↑castSucc i) y) j = update (init q) i y j
simp [init, h]