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

case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin n), append x₀ x (↑(natAdd 1) i) = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) (↑(natAdd 1) i)
case h
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ append x₀ x i = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) i
refine' Fin.addCases _ _ i <;> clear i
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (↑(castAdd n) i) = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) (↑(castAdd n) i)
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin 1), append x₀ x (↑(castAdd n) i) = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) (↑(castAdd n) i)
intro i
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (x₀ 0) x (↑(cast (_ : 1 + n = n + 1)) (↑(castAdd n) 0)) = x₀ 0
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (↑(castAdd n) i) = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) (↑(castAdd n) i)
rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
no goals
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (x₀ 0) x (↑(cast (_ : 1 + n = n + 1)) (↑(castAdd n) 0)) = x₀ 0
exact Fin.cons_zero _ _
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ append x₀ x (↑(natAdd 1) i) = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) (↑(natAdd 1) i)
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin n), append x₀ x (↑(natAdd 1) i) = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) (↑(natAdd 1) i)
intro i
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x (succ i) = x i
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ append x₀ x (↑(natAdd 1) i) = (cons (x₀ 0) x ∘ ↑(cast (_ : 1 + n = n + 1))) (↑(natAdd 1) i)
rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
no goals
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x (succ i) = x i
exact Fin.cons_succ _ _ _