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