-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_last (x : α (last n)) (p : ∀ j : Fin n, α ((last n).succAbove j)) :
    insertNth (last n) x p =
      snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (p j) (cast ⋯ (p j))

Tactic:
exact (cast_heq _ _).symm

Result:
no goals

Proof state:
case a
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ j.castSucc = (last n).succAbove j

Tactic:
rw [succAbove_last]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (p j) (snoc (fun j => cast ⋯ (p j)) x j.castSucc)

Tactic:
rw [snoc_castSucc]

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (p j) (cast ⋯ (p j))

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (snoc (fun j => cast ⋯ (p j)) x j.castSucc) ((last n).removeNth (snoc (fun j => cast ⋯ (p j)) x) j)

Tactic:
apply congr_arg_heq

Result:
case a
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ j.castSucc = (last n).succAbove j

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j = (last n).removeNth (snoc (fun j => cast ⋯ (p j)) x) j

Tactic:
apply eq_of_heq

Result:
case h.h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (p j) ((last n).removeNth (snoc (fun j => cast ⋯ (p j)) x) j)

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ x = snoc (fun j => cast ⋯ (p j)) x (last n)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ p = (last n).removeNth (snoc (fun j => cast ⋯ (p j)) x)

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j = (last n).removeNth (snoc (fun j => cast ⋯ (p j)) x) j

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ (last n).insertNth x p = snoc (fun j => cast ⋯ (p j)) x

Tactic:
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ p = (last n).removeNth (snoc (fun j => cast ⋯ (p j)) x)

Proof state:
case h.h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (p j) ((last n).removeNth (snoc (fun j => cast ⋯ (p j)) x) j)

Tactic:
trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x j.castSucc

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (p j) (snoc (fun j => cast ⋯ (p j)) x j.castSucc)

n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (snoc (fun j => cast ⋯ (p j)) x j.castSucc) ((last n).removeNth (snoc (fun j => cast ⋯ (p j)) x) j)