if hx : x[l]'(Nat.lt_trans hl hk) > x[k] then
  simp only [dif_pos hx, Array.nodup_push, Array.mem_push, ivs'_nodup, true_and]
  constructor
  . intro h
    specialize ivs'_lt _ h; dsimp at ivs'_lt
    refine ivs'_lt.elim ?_ ?_
    . exact Nat.lt_irrefl k
    . intro h; exact Nat.lt_irrefl l h.2
  . intro iv hiv
    cases hiv with
    | inl hmem =>
      refine Or.imp_right ?_ <| ivs'_lt iv hmem
      exact And.imp_right Nat.le.step
    | inr heq =>
      cases heq; dsimp
      exact Or.inr ⟨rfl, l.lt_succ_self⟩
else
  simp only [dif_neg hx]
  apply And.intro ivs'_nodup
  intro iv hiv; specialize ivs'_lt iv hiv
  refine Or.imp_right ?_ ivs'_lt
  exact And.imp_right Nat.le.step
case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ Array.Nodup
      (if h : x[l] > x[k] then
        Array.push ivs'
          { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
            lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
            inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
      else ivs') ∧
    ∀ (iv : Inversion x),
      (iv ∈
          if h : x[l] > x[k] then
            Array.push ivs'
              { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
          else ivs') →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
no goals