m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
⊢ p = fun j =>
    snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j)
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
⊢ insertNth (last n) x p = snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x
refine' insertNth_eq_iff.2 ⟨by simp, _⟩
case h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ p j =
    snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j)
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
⊢ p = fun j =>
    snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j)
ext j
case h.h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (p j)
    (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j))
case h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ p j =
    snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j)
apply eq_of_heq
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (p j) (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑castSucc j))

m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑castSucc j))
    (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j))
case h.h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (p j)
    (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j))
trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x (castSucc j)
no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
⊢ snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (last n) = x
simp
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (p j) (_root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j))
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (p j) (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑castSucc j))
rw [snoc_castSucc]
no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (p j) (_root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j))
exact (cast_heq _ _).symm
case a
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ ↑castSucc j = ↑(succAbove (last n)) j
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ HEq (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑castSucc j))
    (snoc (fun j => _root_.cast (_ : α (↑(succAbove (last n)) j) = α (↑castSucc j)) (p j)) x (↑(succAbove (last n)) j))
apply congr_arg_heq
no goals
case a
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (↑(succAbove (last n)) j)
j : Fin n
⊢ ↑castSucc j = ↑(succAbove (last n)) j
rw [succAbove_last]