n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ (if x : Fin.succ i = 0 then 0 else f (Fin.pred (Fin.succ i) x)) = f i
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ shiftFun f (Fin.succ i) = f i
dsimp [shiftFun]
case inl
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : Fin.succ i = 0
⊢ 0 = f i

case inr
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : ¬Fin.succ i = 0
⊢ f (Fin.pred (Fin.succ i) h) = f i
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ (if x : Fin.succ i = 0 then 0 else f (Fin.pred (Fin.succ i) x)) = f i
split_ifs with h
case inl.h
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : Fin.succ i = 0
⊢ False
case inl
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : Fin.succ i = 0
⊢ 0 = f i
exfalso
no goals
case inl.h
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : Fin.succ i = 0
⊢ False
simp only [Fin.ext_iff, Fin.val_succ, Fin.val_zero, add_eq_zero, and_false] at h
no goals
case inr
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : ¬Fin.succ i = 0
⊢ f (Fin.pred (Fin.succ i) h) = f i
simp only [Fin.pred_succ]