m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (↑(succAbove 0) j)
⊢ p = fun j => cons x (fun j => _root_.cast (_ : α (↑(succAbove 0) j) = α (succ j)) (p j)) (↑(succAbove 0) j)
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (↑(succAbove 0) j)
⊢ insertNth 0 x p = cons x fun j => _root_.cast (_ : α (↑(succAbove 0) j) = α (succ j)) (p j)
refine' insertNth_eq_iff.2 ⟨by simp, _⟩
case h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (↑(succAbove 0) j)
j : Fin n
⊢ p j = cons x (fun j => _root_.cast (_ : α (↑(succAbove 0) j) = α (succ j)) (p j)) (↑(succAbove 0) j)
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (↑(succAbove 0) j)
⊢ p = fun j => cons x (fun j => _root_.cast (_ : α (↑(succAbove 0) j) = α (succ j)) (p j)) (↑(succAbove 0) j)
ext j
no goals
case h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (↑(succAbove 0) j)
j : Fin n
⊢ p j = cons x (fun j => _root_.cast (_ : α (↑(succAbove 0) j) = α (succ j)) (p j)) (↑(succAbove 0) j)
convert (cons_succ x p j).symm
no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (↑(succAbove 0) j)
⊢ cons x (fun j => _root_.cast (_ : α (↑(succAbove 0) j) = α (succ j)) (p j)) 0 = x
simp