apply Option.some_inj.mp
case mk
n j : Nat
hj : j < n
⊢ get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }
case mk
n j : Nat
hj : j < n
⊢ some (get (fins n) { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }