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)
⊢ p (castLT (↑castSucc i) (_ : ↑i < n)) = p 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)
⊢ snoc p x (↑castSucc i) = p i
simp only [snoc, coe_castSucc, is_lt, cast_eq, dite_true]
no goals
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)
⊢ p (castLT (↑castSucc i) (_ : ↑i < n)) = p i
convert cast_eq rfl (p i)