rfl
case refl
n i : Nat
h : i + 1 < n
hlt : { val := i, isLt := (_ : i < n) } < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑{ val := i, isLt := (_ : i < n) } then { val := i + 1, isLt := h }
    else
      { val := ↑{ val := i, isLt := (_ : i < n) },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i, isLt := (_ : i < n) }) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑{ val := i, isLt := (_ : i < n) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
no goals