if hik : i = k.1 then
  have : ⟨i, Nat.lt_of_succ_lt h⟩ = k := Fin.eq_of_val_eq hik
  cases this; rfl
else
  exfalso
  conv at hinv => simp only [hik, if_neg]; change k.1 > i
  exact Nat.not_le_of_lt hlt hinv
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, 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