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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ ↑(natAdd m)) i = snoc (f ∘ ↑(natAdd m)) a 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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
⊢ snoc f a ∘ ↑(natAdd m) = snoc (f ∘ ↑(natAdd m)) a
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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ ↑(natAdd m)) (last n) = snoc (f ∘ ↑(natAdd m)) a (last n)

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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ ↑(natAdd m)) (↑castSucc i) = snoc (f ∘ ↑(natAdd m)) a (↑castSucc 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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ ↑(natAdd m)) i = snoc (f ∘ ↑(natAdd m)) a i
refine' Fin.lastCases _ (fun i ↦ _) 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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (↑(natAdd m) (last n)) = snoc (f ∘ ↑(natAdd m)) a (last n)
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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ ↑(natAdd m)) (last n) = snoc (f ∘ ↑(natAdd m)) a (last n)
simp only [Function.comp_apply]
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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (↑(natAdd m) (last n)) = snoc (f ∘ ↑(natAdd m)) a (last n)
rw [snoc_last, natAdd_last, snoc_last]
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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ snoc f a (↑(natAdd m) (↑castSucc i)) = f (↑(natAdd m) 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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ ↑(natAdd m)) (↑castSucc i) = snoc (f ∘ ↑(natAdd m)) a (↑castSucc i)
simp only [comp_apply, snoc_castSucc]
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✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ snoc f a (↑(natAdd m) (↑castSucc i)) = f (↑(natAdd m) i)
rw [natAdd_castSucc, snoc_castSucc]