revert hj
case mk
n j : Nat
hj : j < length (fins n)
⊢ get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }
case mk
n j : Nat
⊢ ∀ (hj : j < length (fins n)), get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }