m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), insertNth i x p (↑(succAbove i) x_1) = p x_1
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), (insertNth i x p ∘ ↑(succAbove i)) x_1 = p x_1
unfold comp
no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), insertNth i x p (↑(succAbove i) x_1) = p x_1
exact insertNth_apply_succAbove i _ _