simp only [Nat.ne_of_gt <| .step hj, Nat.ne_of_gt hj, if_neg]
n i : Nat
h : i + 1 < n
j : Nat
hj : j < i
hj' : j < n
⊢ (if i + 1 = j then { val := i, isLt := (_ : i < n) }
    else
      if i = j then { val := i + 1, isLt := h }
      else
        { val := j,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) j) }) =
    { val := j, isLt := hj' }
no goals