case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ update (cons x p) 0 z = cons z p
ext j
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z j = cons z p j

case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ update (cons x p) 0 z j = cons z p j
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j
by_cases h : j = 0
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z 0 = cons z p 0
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z j = cons z p j
rw [h]
no goals
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z 0 = cons z p 0
simp
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x p j = cons z p j
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ update (cons x p) 0 z j = cons z p j
simp only [h, update_noteq, Ne.def, not_false_iff]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
⊢ cons x p j = cons z p j
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x p j = cons z p j
let j' := pred j h
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ cons x p j = cons z p j
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
⊢ cons x p j = cons z p j
have : j'.succ = j := succ_pred j h
no goals
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ cons x p j = cons z p j
rw [← this, cons_succ, cons_succ]