case h
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
a : Fin (n + 1)
⊢ ↑(cons (↑t 0) (tail t)) a = ↑t a
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
⊢ cons (↑t 0) (tail t) = t
ext a
case pos
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ ↑(cons (↑t 0) (tail t)) a = ↑t a

case neg
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ ↑(cons (↑t 0) (tail t)) a = ↑t a
case h
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
a : Fin (n + 1)
⊢ ↑(cons (↑t 0) (tail t)) a = ↑t a
by_cases c_a : a = 0
no goals
case pos
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ ↑(cons (↑t 0) (tail t)) a = ↑t a
rw [c_a, cons_zero]
no goals
case neg
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ ↑(cons (↑t 0) (tail t)) a = ↑t a
rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]