no goals
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.32634
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ m + n = n
rw [hu, zero_add]
case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (↑(castAdd n) l) = (v ∘ ↑(cast (_ : m + n = n))) (↑(castAdd n) l)

case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (↑(natAdd m) r) = (v ∘ ↑(cast (_ : m + n = n))) (↑(natAdd m) r)
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
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ ↑(cast (_ : m + n = n))
refine' funext (Fin.addCases (fun l => _) fun r => _)
no goals
case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (↑(castAdd n) l) = (v ∘ ↑(cast (_ : m + n = n))) (↑(castAdd n) l)
exact (Fin.cast hu l).elim0'
case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (↑(cast (_ : m + n = n)) (↑(natAdd m) r))
case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (↑(natAdd m) r) = (v ∘ ↑(cast (_ : m + n = n))) (↑(natAdd m) r)
rw [append_right, Function.comp_apply]
case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ ↑r = ↑(↑(cast (_ : m + n = n)) (↑(natAdd m) r))
case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (↑(cast (_ : m + n = n)) (↑(natAdd m) r))
refine' congr_arg v (Fin.ext _)
no goals
case 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
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ ↑r = ↑(↑(cast (_ : m + n = n)) (↑(natAdd m) r))
simp [hu]