[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
k : Fin n
⊢ ↑(tail (cons y s)) k = ↑s k
[PROOFSTEP]
simp only [tail_apply, cons_succ]
[GOAL]
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
[PROOFSTEP]
ext a
[GOAL]
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
[PROOFSTEP]
by_cases c_a : a = 0
[GOAL]
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
[PROOFSTEP]
rw [c_a, cons_zero]
[GOAL]
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
[PROOFSTEP]
rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]
[GOAL]
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
[PROOFSTEP]
ext a
[GOAL]
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
[PROOFSTEP]
by_cases c : a = 0
[GOAL]
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
[PROOFSTEP]
simp [c]
[GOAL]
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
[PROOFSTEP]
rw [← Fin.succ_pred a c, cons_succ]
[GOAL]
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))
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
h : y ≠ 0
⊢ cons y s ≠ 0
[PROOFSTEP]
contrapose! h with c
[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
c : cons y s = 0
⊢ y = 0
[PROOFSTEP]
rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]
[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
h : s ≠ 0
⊢ cons y s ≠ 0
[PROOFSTEP]
contrapose! h with c
[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
c : cons y s = 0
⊢ s = 0
[PROOFSTEP]
ext a
[GOAL]
case h
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
c : cons y s = 0
a : Fin n
⊢ ↑s a = ↑0 a
[PROOFSTEP]
simp [← cons_succ a y s, c]
[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
⊢ cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩
[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
h : cons y s ≠ 0
⊢ y ≠ 0 ∨ s ≠ 0
[PROOFSTEP]
refine' imp_iff_not_or.1 fun h' c => h _
[GOAL]
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
⊢ cons y s = 0
[PROOFSTEP]
rw [h', c, Finsupp.cons_zero_zero]
