cases iv.fst_eq_or_snd_eq_of_transpos i.lt_succ_self
<;> cases iv <;> rename_i k l hlt hinv heq <;> cases heq
<;> simp only [transposAdj, get_transpos, if_pos] at hinv
n i : Nat
h : i + 1 < n
iv : Inversion (transposAdj i h)
⊢ iv = transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  (if i + 1 = i then { val := i, isLt := (_ : i < n) } else { val := i + 1, isLt := h }) >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑l then { val := i + 1, isLt := h }
      else
        { val := ↑l,
          isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

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 + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      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)