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)
j : Fin (n + 1)
⊢ snoc (init q) (q (last n)) j = q j
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)
⊢ snoc (init q) (q (last n)) = q
ext j
case pos
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)
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (init q) (q (last n)) j = q j

case neg
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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) j = q j
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)
j : Fin (n + 1)
⊢ snoc (init q) (q (last n)) j = q j
by_cases h : j.val < n
case pos
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)
j : Fin (n + 1)
h : ↑j < n
⊢ q (↑castSucc (castLT j (_ : ↑j < n))) = q j
case pos
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)
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (init q) (q (last n)) j = q j
simp only [init, snoc, h, cast_eq, dite_true]
case pos
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)
j : Fin (n + 1)
h : ↑j < n
x✝ : ↑castSucc (castLT j h) = j
⊢ q (↑castSucc (castLT j (_ : ↑j < n))) = q j
case pos
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)
j : Fin (n + 1)
h : ↑j < n
⊢ q (↑castSucc (castLT j (_ : ↑j < n))) = q j
have _ : castSucc (castLT j h) = j := castSucc_castLT _ _
case pos
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)
j : Fin (n + 1)
h : ↑j < n
x✝ : ↑castSucc (castLT j h) = j
⊢ q (↑castSucc (castLT j (_ : ↑j < n))) = _root_.cast (_ : α j = α j) (q j)
case pos
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)
j : Fin (n + 1)
h : ↑j < n
x✝ : ↑castSucc (castLT j h) = j
⊢ q (↑castSucc (castLT j (_ : ↑j < n))) = q j
rw [← cast_eq rfl (q j)]
no goals
case pos
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)
j : Fin (n + 1)
h : ↑j < n
x✝ : ↑castSucc (castLT j h) = j
⊢ q (↑castSucc (castLT j (_ : ↑j < n))) = _root_.cast (_ : α j = α j) (q j)
congr
case neg
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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) (last n) = q (last n)
case neg
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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) j = q j
rw [eq_last_of_not_lt h]
no goals
case neg
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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) (last n) = q (last n)
simp