case h
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i : Fin n✝
y : α✝ (↑castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ append x x₀ = snoc x (x₀ 0)
ext i
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i : Fin n✝
y : α✝ (↑castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (↑(castAdd 1) i) = snoc x (x₀ 0) (↑(castAdd 1) i)

case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i : Fin n✝
y : α✝ (↑castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (↑(natAdd n) i) = snoc x (x₀ 0) (↑(natAdd n) i)
case h
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i
refine' Fin.addCases _ _ i <;> clear i
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (↑(castAdd 1) i) = snoc x (x₀ 0) (↑(castAdd 1) i)
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i : Fin n✝
y : α✝ (↑castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (↑(castAdd 1) i) = snoc x (x₀ 0) (↑(castAdd 1) i)
intro i
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (↑(castAdd 1) i)
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (↑(castAdd 1) i) = snoc x (x₀ 0) (↑(castAdd 1) i)
rw [Fin.append_left]
no goals
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (↑(castAdd 1) i)
exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ append x x₀ (↑(natAdd n) i) = snoc x (x₀ 0) (↑(natAdd n) i)
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i : Fin n✝
y : α✝ (↑castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (↑(natAdd n) i) = snoc x (x₀ 0) (↑(natAdd n) i)
intro i
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (↑(natAdd n) 0)
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ append x x₀ (↑(natAdd n) i) = snoc x (x₀ 0) (↑(natAdd n) i)
rw [Subsingleton.elim i 0, Fin.append_right]
no goals
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (↑castSucc i)
i✝ : Fin n✝
y : α✝ (↑castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (↑(natAdd n) 0)
exact (@snoc_last _ (fun _ => α) _ _).symm