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 0 0) a = ↑0 a
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
⊢ cons 0 0 = 0
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 = 0
⊢ ↑(cons 0 0) a = ↑0 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 = 0
⊢ ↑(cons 0 0) a = ↑0 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 0 0) a = ↑0 a
by_cases c : 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 = 0
⊢ ↑(cons 0 0) a = ↑0 a
simp [c]
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 = 0
⊢ ↑0 (Fin.pred a c) = ↑0 (Fin.succ (Fin.pred a c))
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 = 0
⊢ ↑(cons 0 0) a = ↑0 a
rw [← Fin.succ_pred a c, cons_succ]
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 = 0
⊢ ↑0 (Fin.pred a c) = ↑0 (Fin.succ (Fin.pred a c))
simp