m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ contractNth j op g k = op (g (↑castSucc k)) (g (succ k))
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
⊢ contractNth j op g k = op (g (↑castSucc k)) (g (succ k))
have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
no goals
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ contractNth j op g k = op (g (↑castSucc k)) (g (succ k))
rw [contractNth, if_neg this, if_pos h]