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)
⊢ cons (q 0) (tail q) j = q 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
⊢ cons (q 0) (tail q) = q
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
⊢ cons (q 0) (tail q) j = q 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 (q 0) (tail q) j = q 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)
⊢ cons (q 0) (tail q) j = q 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
⊢ cons (q 0) (tail q) 0 = q 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
⊢ cons (q 0) (tail q) j = q 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
⊢ cons (q 0) (tail q) 0 = q 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
j' : Fin n := pred j h
⊢ cons (q 0) (tail q) j = q 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 (q 0) (tail q) j = q 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 (q 0) (tail q) j = q 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 (q 0) (tail q) j = q j
have : j'.succ = j := succ_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 (q 0) (tail q) (succ j') = q (succ 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
this : succ j' = j
⊢ cons (q 0) (tail q) j = q j
rw [← this]
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 (q 0) (fun i => q (succ i)) (succ j') = q (succ 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
this : succ j' = j
⊢ cons (q 0) (tail q) (succ j') = q (succ j')
unfold tail
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 (q 0) (fun i => q (succ i)) (succ j') = q (succ j')
rw [cons_succ]